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  550  pm5.31  860  dedlem0b  1067  nic-ax  1768  nic-axALT  1769  sylgt  1916  sbimd  2275  2eu6  2680  reuss2  4071  ssuni  4618  omordi  7851  nnawordi  7906  nnmordi  7916  omabs  7932  omsmolem  7938  alephordi  9148  dfac5  9202  dfac2a  9203  fin23lem14  9408  facdiv  13278  facwordi  13280  o1lo1  14553  rlimuni  14566  o1co  14602  rlimcn1  14604  rlimcn2  14606  rlimo1  14632  lo1add  14642  lo1mul  14643  rlimno1  14669  caucvgrlem  14688  caucvgrlem2  14690  gcdcllem1  15502  algcvgblem  15571  isprm5  15698  prmfac1  15710  infpnlem1  15893  gsummptnn0fz  18648  gsummptnn0fzOLD  18649  gsummoncoe1  19947  dmatscmcl  20586  decpmatmulsumfsupp  20857  pmatcollpw1lem1  20858  pmatcollpw2lem  20861  pmatcollpwfi  20866  pm2mpmhmlem1  20902  pm2mp  20909  cpmidpmatlem3  20956  cayhamlem4  20972  isclo2  21172  lmcls  21386  isnrm3  21443  dfconn2  21502  1stcrest  21536  dfac14lem  21700  cnpflf2  22083  isucn2  22362  cncfco  22989  ovolicc2lem3  23577  dyadmbllem  23657  itgcn  23900  aalioulem2  24379  aalioulem3  24380  ulmcn  24444  rlimcxp  24991  o1cxp  24992  chtppilimlem2  25454  chtppilim  25455  pthdlem1  26954  mdsymlem6  29723  crefss  30363  ss2mcls  31913  mclsax  31914  rdgprc  32143  nosupno  32293  nosupres  32297  bj-imim21  32976  bj-axtd  33014  bj-nfimt  33053  bj-ssbim  33058  bj-nfdt  33122  rdgeqoa  33651  pm5.31r  34814  pclclN  35847  isnacs3  37951  syl5imp  39390  imbi12VD  39761  sbcim2gVD  39763  limsupre3lem  40602  sgoldbeven3prm  42347  ply1mulgsumlem3  42845  ply1mulgsumlem4  42846
  Copyright terms: Public domain W3C validator