MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  embantd 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  1947  ax12olem1  1960  el  4322  cantnflem1  7578  ackbij1lem16  8048  fin1a2lem10  8222  inar1  8583  grur1a  8627  sqr2irr  12775  exprmfct  13037  pockthg  13201  drsdirfi  14322  obslbs  16880  iscnp4  17249  isreg2  17363  dfcon2  17403  1stccnp  17446  flftg  17949  cnpfcf  17994  tsmsxp  18105  nmoleub  18636  vitalilem2  19368  vitalilem5  19371  c1lip1  19748  aalioulem6  20121  jensen  20694  2sqlem6  21020  dchrisumlem3  21052  pntlem3  21170  cvmlift2lem1  24768  cvmlift2lem12  24780  nn0prpwlem  26016  bnj849  28634  spimtNEW7  28845  mapdordlem2  31752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator