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 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  84  exptOLD  179  imbi1d  344  meredith  1673  ax13b  2064  ax12v2  2214  axc15  2451  mo3  2589  mo4  2591  2mo  2673  axprlem2  5385  axprlem1OLD  5389  axprglem  5393  frss  5614  fvn0ssdmfun  7075  tfi  7865  nneneq  9225  wemaplem2  9545  unxpwdom2  9586  cantnfp1lem3  9685  setrec1lem2  9971  infxpenlem  10096  axpowndlem3  10688  indpi  10996  fzind  12801  injresinj  13930  seqcl2  14167  seqfveq2  14171  seqshft2  14175  monoord  14179  seqsplit  14182  seqid2  14195  seqhomo  14196  seqcoll  14613  rexuzre  15526  rexico  15527  limsupbnd2  15656  rlim2lt  15670  rlim3  15671  lo1le  15825  caurcvg  15850  lcmfunsnlem1  16818  coprmprod  16842  eulerthlem2  16965  ramtlecl  17184  sylow1lem1  19818  efgsrel  19954  elcls3  23407  cncls2  23597  cnntr  23599  filssufilg  24236  ufileu  24244  alexsubALTlem3  24374  tgpt0  24444  isucn2  24603  imasdsf1olem  24698  nmoleub2lem2  25443  ovolicc2lem3  25846  dyadmbllem  25926  dvnres  26257  rlimcnp  27299  xrlimcnp  27302  ftalem2  27407  bcmono  27610  2sqlem6  27756  fltaccoprm  27978  fltabcoprm  27980  flt4lem5  27986  mulsproplem13  28520  mulsproplem14  28521  eupth2lems  30845  mdslmd1lem1  32933  xrge0infss  33399  axpowg2  35872  axpowg3  35873  subfacp1lem6  36037  cvmliftlem7  36143  cvmliftlem10  36146  ss2mcls  36420  mclsax  36421  axtco2  37355  bj-imim11  37511  bj-sylget  37596  bj-19.21t  37756  bj-spimt2  37790  findcard4  38726  mettrifi  38785  diaintclN  42209  dibintclN  42318  dihintcl  42495  mapdh9a  42940  posbezout  43244  aks6d1c6lem3  43316  cantnfresb  44420  safesnsupfiub  44511  iunrelexp0  44796  mnuop3d  45349  imbi12VD  45949  monoordxrv  46585  fcoresf1  48233  rexrsb  48264  smonoord  48541  ply1mulgsumlem1  49592  pgindnf  50978