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:  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  el  4585  findcard2d  7668  cantnflem1  8011  cantnflem1OLD  8034  ackbij1lem16  8518  fin1a2lem10  8692  inar1  9056  grur1a  9100  sqr2irr  13652  exprmfct  13917  pockthg  14088  drsdirfi  15230  obslbs  18283  mdetunilem9  18561  iscnp4  19002  isreg2  19116  dfcon2  19158  1stccnp  19201  flftg  19704  cnpfcf  19749  tsmsxp  19864  nmoleub  20445  vitalilem2  21225  vitalilem5  21228  c1lip1  21605  aalioulem6  21939  jensen  22518  2sqlem6  22844  dchrisumlem3  22876  pntlem3  22994  cvmlift2lem1  27355  cvmlift2lem12  27367  nn0prpwlem  28685  lindslinindsimp1  31143  bnj849  32270  bj-el  32669  mapdordlem2  35640
  Copyright terms: Public domain W3C validator