MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  embantd Structured version   Unicode version

Theorem embantd 52
Description: Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.)
Hypotheses
Ref Expression
embantd.1  |-  ( ph  ->  ps )
embantd.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
embantd  |-  ( ph  ->  ( ( ps  ->  ch )  ->  th )
)

Proof of Theorem embantd
StepHypRef Expression
1 embantd.1 . 2  |-  ( ph  ->  ps )
2 embantd.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
32imim2d 50 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpid 39 1  |-  ( ph  ->  ( ( ps  ->  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  spimtOLD  1956  ax12olem1  2005  el  4373  cantnflem1  7637  ackbij1lem16  8107  fin1a2lem10  8281  inar1  8642  grur1a  8686  sqr2irr  12840  exprmfct  13102  pockthg  13266  drsdirfi  14387  obslbs  16949  iscnp4  17319  isreg2  17433  dfcon2  17474  1stccnp  17517  flftg  18020  cnpfcf  18065  tsmsxp  18176  nmoleub  18757  vitalilem2  19493  vitalilem5  19496  c1lip1  19873  aalioulem6  20246  jensen  20819  2sqlem6  21145  dchrisumlem3  21177  pntlem3  21295  cvmlift2lem1  24981  cvmlift2lem12  24993  nn0prpwlem  26316  bnj849  29233  spimtNEW7  29444  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator