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  180  imbi1d  345  meredith  1643  ax13b  2039  ax12v2  2177  axc15  2433  sbequiALT  2572  mo3  2623  mo4  2625  2mo  2710  sstr2  3922  ssralv  3981  axprlem1  5289  axprlem2  5290  axpr  5294  frss  5486  fvn0ssdmfun  6819  tfi  7548  nneneq  8684  wemaplem2  8995  unxpwdom2  9036  cantnfp1lem3  9127  infxpenlem  9424  axpowndlem3  10010  indpi  10318  fzind  12068  injresinj  13153  seqcl2  13384  seqfveq2  13388  seqshft2  13392  monoord  13396  seqsplit  13399  seqid2  13412  seqhomo  13413  seqcoll  13818  rexuzre  14704  rexico  14705  limsupbnd2  14832  rlim2lt  14846  rlim3  14847  lo1le  15000  caurcvg  15025  lcmfunsnlem1  15971  coprmprod  15995  eulerthlem2  16109  ramtlecl  16326  sylow1lem1  18715  efgsrel  18852  elcls3  21688  cncls2  21878  cnntr  21880  filssufilg  22516  ufileu  22524  alexsubALTlem3  22654  tgpt0  22724  isucn2  22885  imasdsf1olem  22980  nmoleub2lem2  23721  ovolicc2lem3  24123  dyadmbllem  24203  dvnres  24534  rlimcnp  25551  xrlimcnp  25554  ftalem2  25659  bcmono  25861  2sqlem6  26007  eupth2lems  28023  mdslmd1lem1  30108  xrge0infss  30510  subfacp1lem6  32545  cvmliftlem7  32651  cvmliftlem10  32654  ss2mcls  32928  mclsax  32929  bj-sylget  34067  bj-nfimt  34084  bj-19.21t  34213  bj-19.37im  34216  bj-spimt2  34222  mettrifi  35195  diaintclN  38354  dibintclN  38463  dihintcl  38640  mapdh9a  39085  iunrelexp0  40403  mnuop3d  40979  imbi12VD  41579  monoordxrv  42121  rexrsb  43655  smonoord  43888  ply1mulgsumlem1  44794  setrec1lem2  45218