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  177  imbi1d  341  meredith  1642  ax13b  2033  ax12v2  2182  axc15  2422  mo3  2559  mo4  2561  2mo  2643  sstr2OLD  3942  ssralvOLD  4007  axprlem1  5361  axprlem2  5362  axprOLD  5369  frss  5580  fvn0ssdmfun  7007  tfi  7783  nneneq  9115  wemaplem2  9433  unxpwdom2  9474  cantnfp1lem3  9570  infxpenlem  9904  axpowndlem3  10490  indpi  10798  fzind  12571  injresinj  13691  seqcl2  13927  seqfveq2  13931  seqshft2  13935  monoord  13939  seqsplit  13942  seqid2  13955  seqhomo  13956  seqcoll  14371  rexuzre  15260  rexico  15261  limsupbnd2  15390  rlim2lt  15404  rlim3  15405  lo1le  15559  caurcvg  15584  lcmfunsnlem1  16548  coprmprod  16572  eulerthlem2  16693  ramtlecl  16912  sylow1lem1  19511  efgsrel  19647  elcls3  22999  cncls2  23189  cnntr  23191  filssufilg  23827  ufileu  23835  alexsubALTlem3  23965  tgpt0  24035  isucn2  24194  imasdsf1olem  24289  nmoleub2lem2  25044  ovolicc2lem3  25448  dyadmbllem  25528  dvnres  25861  rlimcnp  26903  xrlimcnp  26906  ftalem2  27012  bcmono  27216  2sqlem6  27362  mulsproplem13  28068  mulsproplem14  28069  eupth2lems  30216  mdslmd1lem1  32303  xrge0infss  32741  subfacp1lem6  35227  cvmliftlem7  35333  cvmliftlem10  35336  ss2mcls  35610  mclsax  35611  bj-sylget  36661  bj-nfimt  36678  bj-19.21t  36809  bj-19.37im  36812  bj-spimt2  36825  mettrifi  37803  diaintclN  41103  dibintclN  41212  dihintcl  41389  mapdh9a  41834  posbezout  42139  aks6d1c6lem3  42211  fltaccoprm  42679  fltabcoprm  42681  flt4lem5  42689  cantnfresb  43363  safesnsupfiub  43455  iunrelexp0  43741  mnuop3d  44310  imbi12VD  44911  monoordxrv  45525  natlocalincr  46920  fcoresf1  47106  rexrsb  47137  smonoord  47408  ply1mulgsumlem1  48424  setrec1lem2  49726  pgindnf  49754