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  556  dedlem0b  1044  nic-ax  1676  nic-axALT  1677  sylgt  1825  axc15  2421  2eu6  2653  reuss2  4276  ssuni  4894  omordi  8514  nnawordi  8569  nnmordi  8579  omabs  8598  omsmolem  8604  unfi  9119  alephordi  10015  dfac5  10069  dfac2a  10070  fin23lem14  10274  facdiv  14193  facwordi  14195  o1lo1  15425  rlimuni  15438  o1co  15474  rlimcn1  15476  rlimcn3  15478  rlimo1  15505  lo1add  15515  lo1mul  15516  rlimno1  15544  caucvgrlem  15563  caucvgrlem2  15565  gcdcllem1  16384  algcvgblem  16458  isprm5  16588  prmfac1  16602  infpnlem1  16787  gsummptnn0fz  19768  gsummoncoe1  21691  dmatscmcl  21868  decpmatmulsumfsupp  22138  pmatcollpw1lem1  22139  pmatcollpw2lem  22142  pmatcollpwfi  22147  pm2mpmhmlem1  22183  pm2mp  22190  cpmidpmatlem3  22237  cayhamlem4  22253  isclo2  22455  lmcls  22669  isnrm3  22726  dfconn2  22786  1stcrest  22820  dfac14lem  22984  cnpflf2  23367  isucn2  23647  cncfco  24286  ovolicc2lem3  24899  dyadmbllem  24979  itgcn  25225  aalioulem2  25709  aalioulem3  25710  ulmcn  25774  rlimcxp  26339  o1cxp  26340  chtppilimlem2  26838  chtppilim  26839  nosupno  27067  nosupres  27071  noinfno  27082  noinfres  27086  pthdlem1  28756  mdsymlem6  31392  evls1fpws  32320  crefss  32487  ss2mcls  34219  mclsax  34220  rdgprc  34425  bj-imim21  35060  bj-axtd  35105  bj-nfimt  35148  bj-nfdt  35207  bj-19.23t  35281  bj-19.36im  35282  rdgeqoa  35887  rdgssun  35895  wl-cbvmotv  36018  pclclN  38400  isnacs3  41076  syl5imp  42882  imbi12VD  43243  sbcim2gVD  43245  limsupre3lem  44059  limsupub2  44139  fcoresf1  45389  sgoldbeven3prm  46061  ply1mulgsumlem3  46555  ply1mulgsumlem4  46556
  Copyright terms: Public domain W3C validator