Theorem imim1d 82

Description: Deduction adding nested consequents. Deduction associated with imim1 83 and imim1i 63. (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 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 81	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  83  expt  170  imbi1d  333  meredith  1685  ax13b  2082  ax12v2  2165  sbequivv  2287  axc15  2387  sbequi  2451  mo3  2580  mo3OLD  2581  2mo  2678  sstr2  3828  ssralv  3885  frss  5322  fvn0ssdmfun  6614  tfi  7331  nneneq  8431  wemaplem2  8741  unxpwdom2  8782  cantnfp1lem3  8874  infxpenlem  9169  axpowndlem3  9756  indpi  10064  fzind  11827  injresinj  12908  seqcl2  13137  seqfveq2  13141  seqshft2  13145  monoord  13149  seqsplit  13152  seqid2  13165  seqhomo  13166  seqcoll  13562  rexuzre  14499  rexico  14500  limsupbnd2  14622  rlim2lt  14636  rlim3  14637  lo1le  14790  caurcvg  14815  lcmfunsnlem1  15756  coprmprod  15780  eulerthlem2  15891  ramtlecl  16108  sylow1lem1  18397  efgsrel  18531  elcls3  21295  cncls2  21485  cnntr  21487  filssufilg  22123  ufileu  22131  alexsubALTlem3  22261  tgpt0  22330  isucn2  22491  imasdsf1olem  22586  nmoleub2lem2  23323  ovolicc2lem3  23723  dyadmbllem  23803  dvnres  24131  rlimcnp  25144  xrlimcnp  25147  ftalem2  25252  bcmono  25454  2sqlem6  25600  eupth2lems  27642  mdslmd1lem1  29756  xrge0infss  30090  subfacp1lem6  31766  cvmliftlem7  31872  cvmliftlem10  31875  ss2mcls  32064  mclsax  32065  bj-exlimh  33181  bj-nfimt  33196  bj-spimt2  33297  wl-ax8clv2  34008  mettrifi  34179  diaintclN  37214  dibintclN  37323  dihintcl  37500  mapdh9a  37945  iunrelexp0  38955  imbi12VD  40046  monoordxrv  40621  smonoord  42377  ply1mulgsumlem1  43193  setrec1lem2  43544