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

Theorem imim2d 57
Description: Deduction adding nested antecedents. Deduction associated with imim2 58 and imim2i 16. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
imim2d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imim2d (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))

Proof of Theorem imim2d
StepHypRef Expression
1 imim2d.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32a2d 29 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:  imim2  58  embantd  59  imim12d  81  anc2r  555  dedlem0b  1038  nic-ax  1667  nic-axALT  1668  sylgt  1815  axc15  2440  sbimdvOLD  2514  sbimdOLD  2516  2eu6  2743  reuss2  4287  ssuni  4859  omordi  8182  nnawordi  8237  nnmordi  8247  omabs  8264  omsmolem  8270  alephordi  9489  dfac5  9543  dfac2a  9544  fin23lem14  9744  facdiv  13637  facwordi  13639  o1lo1  14884  rlimuni  14897  o1co  14933  rlimcn1  14935  rlimcn2  14937  rlimo1  14963  lo1add  14973  lo1mul  14974  rlimno1  15000  caucvgrlem  15019  caucvgrlem2  15021  gcdcllem1  15838  algcvgblem  15911  isprm5  16041  prmfac1  16053  infpnlem1  16236  gsummptnn0fz  19026  gsummoncoe1  20389  dmatscmcl  21028  decpmatmulsumfsupp  21297  pmatcollpw1lem1  21298  pmatcollpw2lem  21301  pmatcollpwfi  21306  pm2mpmhmlem1  21342  pm2mp  21349  cpmidpmatlem3  21396  cayhamlem4  21412  isclo2  21612  lmcls  21826  isnrm3  21883  dfconn2  21943  1stcrest  21977  dfac14lem  22141  cnpflf2  22524  isucn2  22803  cncfco  23430  ovolicc2lem3  24035  dyadmbllem  24115  itgcn  24358  aalioulem2  24837  aalioulem3  24838  ulmcn  24902  rlimcxp  25465  o1cxp  25466  chtppilimlem2  25964  chtppilim  25965  pthdlem1  27461  mdsymlem6  30099  crefss  30999  ss2mcls  32699  mclsax  32700  rdgprc  32923  nosupno  33087  nosupres  33091  bj-imim21  33770  bj-axtd  33812  bj-nfimt  33855  bj-nfdt  33914  bj-19.23t  33983  bj-19.36im  33984  rdgeqoa  34520  rdgssun  34528  wl-cbvmotv  34622  pclclN  36894  isnacs3  39172  syl5imp  40711  imbi12VD  41072  sbcim2gVD  41074  limsupre3lem  41878  limsupub2  41958  sgoldbeven3prm  43780  ply1mulgsumlem3  44274  ply1mulgsumlem4  44275
  Copyright terms: Public domain W3C validator