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  870  mo2v  2505  el  4877  fpropnf1  6564  findcard2d  8243  cantnflem1  8624  ackbij1lem16  9095  fin1a2lem10  9269  inar1  9635  grur1a  9679  sqrt2irr  15023  lcmf  15393  lcmfunsnlem  15401  exprmfct  15463  pockthg  15657  prmgaplem5  15806  prmgaplem6  15807  drsdirfi  16985  obslbs  20122  mdetunilem9  20474  iscnp4  21115  isreg2  21229  dfconn2  21270  1stccnp  21313  flftg  21847  cnpfcf  21892  tsmsxp  22005  nmoleub  22582  vitalilem2  23423  vitalilem5  23426  c1lip1  23805  aalioulem6  24137  jensen  24760  2sqlem6  25193  dchrisumlem3  25225  pntlem3  25343  finsumvtxdg2sstep  26501  bnj849  31121  cvmlift2lem1  31410  cvmlift2lem12  31422  mclsax  31592  nn0prpwlem  32442  bj-el  32921  matunitlindflem1  33535  poimirlem30  33569  mapdordlem2  37243  iccelpart  41694  sbgoldbalt  41994  sbgoldbm  41997  evengpop3  42011  evengpoap3  42012  bgoldbtbnd  42022  lindslinindsimp1  42571
 Copyright terms: Public domain W3C validator