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  1043  nic-ax  1675  nic-axALT  1676  sylgt  1824  axc15  2420  2eu6  2656  reuss2  4273  ssuni  4891  omordi  8505  nnawordi  8560  nnmordi  8570  omabs  8589  omsmolem  8595  unfi  9074  alephordi  9968  dfac5  10022  dfac2a  10023  fin23lem14  10227  facdiv  14141  facwordi  14143  o1lo1  15373  rlimuni  15386  o1co  15422  rlimcn1  15424  rlimcn3  15426  rlimo1  15453  lo1add  15463  lo1mul  15464  rlimno1  15492  caucvgrlem  15511  caucvgrlem2  15513  gcdcllem1  16333  algcvgblem  16407  isprm5  16537  prmfac1  16551  infpnlem1  16736  gsummptnn0fz  19716  gsummoncoe1  21621  dmatscmcl  21798  decpmatmulsumfsupp  22068  pmatcollpw1lem1  22069  pmatcollpw2lem  22072  pmatcollpwfi  22077  pm2mpmhmlem1  22113  pm2mp  22120  cpmidpmatlem3  22167  cayhamlem4  22183  isclo2  22385  lmcls  22599  isnrm3  22656  dfconn2  22716  1stcrest  22750  dfac14lem  22914  cnpflf2  23297  isucn2  23577  cncfco  24216  ovolicc2lem3  24829  dyadmbllem  24909  itgcn  25155  aalioulem2  25639  aalioulem3  25640  ulmcn  25704  rlimcxp  26269  o1cxp  26270  chtppilimlem2  26768  chtppilim  26769  nosupno  26997  nosupres  27001  noinfno  27012  noinfres  27016  pthdlem1  28559  mdsymlem6  31195  evls1fpws  32108  crefss  32258  ss2mcls  33990  mclsax  33991  rdgprc  34201  bj-imim21  34946  bj-axtd  34991  bj-nfimt  35034  bj-nfdt  35093  bj-19.23t  35167  bj-19.36im  35168  rdgeqoa  35773  rdgssun  35781  wl-cbvmotv  35904  pclclN  38286  isnacs3  40936  syl5imp  42699  imbi12VD  43060  sbcim2gVD  43062  limsupre3lem  43868  limsupub2  43948  fcoresf1  45198  sgoldbeven3prm  45870  ply1mulgsumlem3  46364  ply1mulgsumlem4  46365
  Copyright terms: Public domain W3C validator