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  578  pm5.31  611  dedlem0b  1013  nic-ax  1638  nic-axALT  1639  sylgt  1789  nfimt  1861  nfimdOLD  2262  2eu6  2587  reuss2  3940  ssuni  4491  ssuniOLD  4492  omordi  7691  nnawordi  7746  nnmordi  7756  omabs  7772  omsmolem  7778  alephordi  8935  dfac5  8989  dfac2a  8990  fin23lem14  9193  facdiv  13114  facwordi  13116  o1lo1  14312  rlimuni  14325  o1co  14361  rlimcn1  14363  rlimcn2  14365  rlimo1  14391  lo1add  14401  lo1mul  14402  rlimno1  14428  caucvgrlem  14447  caucvgrlem2  14449  gcdcllem1  15268  algcvgblem  15337  isprm5  15466  prmfac1  15478  infpnlem1  15661  gsummptnn0fz  18428  gsummoncoe1  19722  dmatscmcl  20357  decpmatmulsumfsupp  20626  pmatcollpw1lem1  20627  pmatcollpw2lem  20630  pmatcollpwfi  20635  pm2mpmhmlem1  20671  pm2mp  20678  cpmidpmatlem3  20725  cayhamlem4  20741  isclo2  20940  lmcls  21154  isnrm3  21211  dfconn2  21270  1stcrest  21304  dfac14lem  21468  cnpflf2  21851  isucn2  22130  cncfco  22757  ovolicc2lem3  23333  dyadmbllem  23413  itgcn  23654  aalioulem2  24133  aalioulem3  24134  ulmcn  24198  rlimcxp  24745  o1cxp  24746  chtppilimlem2  25208  chtppilim  25209  pthdlem1  26718  mdsymlem6  29395  crefss  30044  ss2mcls  31591  mclsax  31592  rdgprc  31824  nosupno  31974  nosupres  31978  bj-imim21  32664  bj-axtd  32703  bj-ssbim  32746  bj-nfdt  32811  rdgeqoa  33348  pm5.31r  34462  pclclN  35495  isnacs3  37590  syl5imp  39035  imbi12VD  39423  sbcim2gVD  39425  limsupre3lem  40282  sgoldbeven3prm  41996  ply1mulgsumlem3  42501  ply1mulgsumlem4  42502
  Copyright terms: Public domain W3C validator