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

Theorem embantd 59
Description: Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.)
Hypotheses
Ref Expression
embantd.1 (𝜑𝜓)
embantd.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
embantd (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem embantd
StepHypRef Expression
1 embantd.1 . 2 (𝜑𝜓)
2 embantd.2 . . 3 (𝜑 → (𝜒𝜃))
32imim2d 57 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
41, 3mpid 44 1 (𝜑 → ((𝜓𝜒) → 𝜃))
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  888  mo2v  2614  el  4996  fpropnf1  6688  findcard2d  8369  cantnflem1  8761  ackbij1lem16  9269  fin1a2lem10  9443  inar1  9809  grur1a  9853  sqrt2irr  15198  lcmf  15568  lcmfunsnlem  15576  exprmfct  15638  pockthg  15832  prmgaplem5  15981  prmgaplem6  15982  drsdirfi  17159  obslbs  20296  mdetunilem9  20648  iscnp4  21289  isreg2  21403  dfconn2  21444  1stccnp  21487  flftg  22021  cnpfcf  22066  tsmsxp  22179  nmoleub  22756  vitalilem2  23597  vitalilem5  23600  c1lip1  23979  aalioulem6  24311  jensen  24935  2sqlem6  25368  dchrisumlem3  25400  pntlem3  25518  finsumvtxdg2sstep  26676  bnj849  31323  cvmlift2lem1  31612  cvmlift2lem12  31624  mclsax  31794  nn0prpwlem  32644  bj-el  33124  matunitlindflem1  33736  poimirlem30  33770  mapdordlem2  37446  iccelpart  41897  sbgoldbalt  42197  sbgoldbm  42200  evengpop3  42214  evengpoap3  42215  bgoldbtbnd  42225  lindslinindsimp1  42774
  Copyright terms: Public domain W3C validator