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  1914  el  4192  cantnflem1  7391  ackbij1lem16  7861  fin1a2lem10  8035  inar1  8397  grur1a  8441  sqr2irr  12527  exprmfct  12789  pockthg  12953  drsdirfi  14072  obslbs  16630  isreg2  17105  dfcon2  17145  1stccnp  17188  flftg  17691  cnpfcf  17736  tsmsxp  17837  nmoleub  18240  vitalilem2  18964  vitalilem5  18967  c1lip1  19344  aalioulem6  19717  jensen  20283  2sqlem6  20608  dchrisumlem3  20640  pntlem3  20758  cvmlift2lem1  23833  cvmlift2lem12  23845  iscnp4  25563  nn0prpwlem  26238  bnj849  28957  mapdordlem2  31827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator