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  1674  ax13b  2067  ax12v2  2218  axc15  2454  mo3  2592  mo4  2594  2mo  2676  axprlem2  5391  axprlem1OLD  5395  axprglem  5399  frss  5620  fvn0ssdmfun  7101  tfi  7891  nneneq  9252  wemaplem2  9571  unxpwdom2  9612  cantnfp1lem3  9711  setrec1lem2  9997  infxpenlem  10122  axpowndlem3  10714  indpi  11022  fzind  12827  injresinj  13956  seqcl2  14193  seqfveq2  14197  seqshft2  14201  monoord  14205  seqsplit  14208  seqid2  14221  seqhomo  14222  seqcoll  14639  rexuzre  15552  rexico  15553  limsupbnd2  15682  rlim2lt  15696  rlim3  15697  lo1le  15851  caurcvg  15876  lcmfunsnlem1  16844  coprmprod  16868  eulerthlem2  16991  ramtlecl  17210  sylow1lem1  19845  efgsrel  19981  elcls3  23434  cncls2  23624  cnntr  23626  filssufilg  24263  ufileu  24271  alexsubALTlem3  24401  tgpt0  24471  isucn2  24630  imasdsf1olem  24725  nmoleub2lem2  25470  ovolicc2lem3  25873  dyadmbllem  25953  dvnres  26284  rlimcnp  27326  xrlimcnp  27329  ftalem2  27434  bcmono  27637  2sqlem6  27783  fltaccoprm  28005  fltabcoprm  28007  flt4lem5  28013  mulsproplem13  28547  mulsproplem14  28548  eupth2lems  30872  mdslmd1lem1  32960  xrge0infss  33425  axpowg2  35928  axpowg3  35929  subfacp1lem6  36130  cvmliftlem7  36236  cvmliftlem10  36239  ss2mcls  36513  mclsax  36514  axtco2  37453  bj-imim11  37609  bj-sylget  37694  bj-19.21t  37854  bj-spimt2  37888  findcard4  38837  mettrifi  38894  diaintclN  42318  dibintclN  42427  dihintcl  42604  mapdh9a  43049  posbezout  43353  aks6d1c6lem3  43425  cantnfresb  44529  safesnsupfiub  44620  iunrelexp0  44905  mnuop3d  45458  imbi12VD  46057  monoordxrv  46706  fcoresf1  48354  rexrsb  48386  smonoord  48662  ply1mulgsumlem1  49713  pgindnf  51099