Theorem imim1d 83

Description: Deduction adding nested consequents. Deduction associated with imim1 84 and imim1i 64. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Hypothesis

Ref	Expression
imim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imim1d	⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

Proof of Theorem imim1d

Step	Hyp	Ref	Expression
1		imim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 82	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim1  84  exptOLD  179  imbi1d  344  meredith  1671  ax13b  2062  ax12v2  2215  axc15  2454  mo3  2592  mo4  2594  2mo  2676  axprlem2  5397  axprlem1OLD  5401  axprOLD  5405  axprglem  5409  frss  5627  fvn0ssdmfun  7071  tfi  7850  nneneq  9191  wemaplem2  9510  unxpwdom2  9551  cantnfp1lem3  9650  infxpenlem  9998  axpowndlem3  10585  indpi  10893  fzind  12695  injresinj  13822  seqcl2  14058  seqfveq2  14062  seqshft2  14066  monoord  14070  seqsplit  14073  seqid2  14086  seqhomo  14087  seqcoll  14503  rexuzre  15406  rexico  15407  limsupbnd2  15536  rlim2lt  15550  rlim3  15551  lo1le  15705  caurcvg  15730  lcmfunsnlem1  16696  coprmprod  16720  eulerthlem2  16842  ramtlecl  17061  sylow1lem1  19669  efgsrel  19805  elcls3  23221  cncls2  23411  cnntr  23413  filssufilg  24049  ufileu  24057  alexsubALTlem3  24187  tgpt0  24257  isucn2  24416  imasdsf1olem  24511  nmoleub2lem2  25256  ovolicc2lem3  25659  dyadmbllem  25739  dvnres  26071  rlimcnp  27111  xrlimcnp  27114  ftalem2  27219  bcmono  27422  2sqlem6  27568  mulsproplem13  28302  mulsproplem14  28303  eupth2lems  30570  mdslmd1lem1  32658  xrge0infss  33086  axpowg2  35541  axpowg3  35542  subfacp1lem6  35658  cvmliftlem7  35764  cvmliftlem10  35767  ss2mcls  36041  mclsax  36042  axtco2  36966  bj-imim11  37122  bj-sylget  37207  bj-19.21t  37367  bj-spimt2  37401  mettrifi  38389  diaintclN  41813  dibintclN  41922  dihintcl  42099  mapdh9a  42544  posbezout  42848  aks6d1c6lem3  42920  fltaccoprm  43355  fltabcoprm  43357  flt4lem5  43365  cantnfresb  44034  safesnsupfiub  44125  iunrelexp0  44411  mnuop3d  44964  imbi12VD  45564  monoordxrv  46178  natlocalincr  47575  fcoresf1  47789  rexrsb  47820  smonoord  48097  ply1mulgsumlem1  49149  setrec1lem2  50449  pgindnf  50477