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

Theorem embantd 54
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 52 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpid 41 1  |-  ( ph  ->  ( ( ps  ->  ch )  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  a2and  809  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  el  4615  findcard2d  7760  cantnflem1  8106  cantnflem1OLD  8129  ackbij1lem16  8613  fin1a2lem10  8787  inar1  9151  grur1a  9195  sqrt2irr  13854  exprmfct  14123  pockthg  14296  drsdirfi  15436  obslbs  18628  mdetunilem9  18989  iscnp4  19630  isreg2  19744  dfcon2  19786  1stccnp  19829  flftg  20363  cnpfcf  20408  tsmsxp  20523  nmoleub  21104  vitalilem2  21884  vitalilem5  21887  c1lip1  22264  aalioulem6  22598  jensen  23183  2sqlem6  23509  dchrisumlem3  23541  pntlem3  23659  cvmlift2lem1  28613  cvmlift2lem12  28625  mclsax  28795  nn0prpwlem  30108  lindslinindsimp1  32768  bnj849  33690  bj-el  34094  mapdordlem2  37066
  Copyright terms: Public domain W3C validator