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

Theorem embantd 50
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 48 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpid 37 1  |-  ( ph  ->  ( ( ps  ->  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  spimt  1927  el  4208  cantnflem1  7407  ackbij1lem16  7877  fin1a2lem10  8051  inar1  8413  grur1a  8457  sqr2irr  12543  exprmfct  12805  pockthg  12969  drsdirfi  14088  obslbs  16646  isreg2  17121  dfcon2  17161  1stccnp  17204  flftg  17707  cnpfcf  17752  tsmsxp  17853  nmoleub  18256  vitalilem2  18980  vitalilem5  18983  c1lip1  19360  aalioulem6  19733  jensen  20299  2sqlem6  20624  dchrisumlem3  20656  pntlem3  20774  cvmlift2lem1  23848  cvmlift2lem12  23860  iscnp4  25666  nn0prpwlem  26341  bnj849  29273  spimtNEW7  29484  mapdordlem2  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator