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  579  pm5.31  612  dedlem0b  1001  nic-ax  1597  nic-axALT  1598  sylgt  1748  nfimt  1820  nfimdOLD  2225  2eu6  2557  reuss2  3905  ssuni  4457  ssuniOLD  4458  omordi  7643  nnawordi  7698  nnmordi  7708  omabs  7724  omsmolem  7730  alephordi  8894  dfac5  8948  dfac2a  8949  fin23lem14  9152  facdiv  13069  facwordi  13071  o1lo1  14262  rlimuni  14275  o1co  14311  rlimcn1  14313  rlimcn2  14315  rlimo1  14341  lo1add  14351  lo1mul  14352  rlimno1  14378  caucvgrlem  14397  caucvgrlem2  14399  gcdcllem1  15215  algcvgblem  15284  isprm5  15413  prmfac1  15425  infpnlem1  15608  gsummptnn0fz  18376  gsummoncoe1  19668  dmatscmcl  20303  decpmatmulsumfsupp  20572  pmatcollpw1lem1  20573  pmatcollpw2lem  20576  pmatcollpwfi  20581  pm2mpmhmlem1  20617  pm2mp  20624  cpmidpmatlem3  20671  cayhamlem4  20687  isclo2  20886  lmcls  21100  isnrm3  21157  dfconn2  21216  1stcrest  21250  dfac14lem  21414  cnpflf2  21798  isucn2  22077  cncfco  22704  ovolicc2lem3  23281  dyadmbllem  23361  itgcn  23603  aalioulem2  24082  aalioulem3  24083  ulmcn  24147  rlimcxp  24694  o1cxp  24695  chtppilimlem2  25157  chtppilim  25158  pthdlem1  26656  mdsymlem6  29251  crefss  29901  ss2mcls  31450  mclsax  31451  rdgprc  31684  nosupno  31833  nosupres  31837  bj-imim21  32523  bj-axtd  32562  bj-ssbim  32605  bj-nfdt  32670  rdgeqoa  33198  pm5.31r  33969  pclclN  35003  isnacs3  37099  syl5imp  38544  imbi12VD  38935  sbcim2gVD  38937  limsupre3lem  39770  sgoldbeven3prm  41442  ply1mulgsumlem3  41947  ply1mulgsumlem4  41948
  Copyright terms: Public domain W3C validator