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

Theorem embantd 56
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 54 . 2  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
41, 3mpid 42 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  825  mo2v  2316  el  4598  findcard2d  7838  cantnflem1  8219  ackbij1lem16  8690  fin1a2lem10  8864  inar1  9225  grur1a  9269  sqrt2irr  14349  lcmf  14654  lcmfunsnlem  14662  exprmfct  14696  pockthg  14898  prmgaplem5  15073  prmgaplem6  15074  drsdirfi  16231  obslbs  19341  mdetunilem9  19693  iscnp4  20327  isreg2  20441  dfcon2  20482  1stccnp  20525  flftg  21059  cnpfcf  21104  tsmsxp  21217  nmoleub  21784  nmoleubOLD  21800  vitalilem2  22615  vitalilem5  22618  c1lip1  22997  aalioulem6  23341  jensen  23962  2sqlem6  24345  dchrisumlem3  24377  pntlem3  24495  bnj849  29784  cvmlift2lem1  30073  cvmlift2lem12  30085  mclsax  30255  nn0prpwlem  31026  bj-el  31455  poimirlem30  32014  mapdordlem2  35249  iccelpart  38784  sgoldbalt  38919  evengpop3  38930  evengpoap3  38931  bgoldbtbnd  38941  fpropnf1  39077  lindslinindsimp1  40522
  Copyright terms: Public domain W3C validator