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  179  imbi1d  344  meredith  1641  ax13b  2038  ax12v2  2178  sbequivvOLD  2333  axc15  2443  sbequiOLD  2533  sbequiALT  2595  mo3  2647  mo4  2649  2mo  2732  sstr2  3977  ssralv  4036  axprlem1  5327  axprlem2  5328  axpr  5332  frss  5525  fvn0ssdmfun  6845  tfi  7571  nneneq  8703  wemaplem2  9014  unxpwdom2  9055  cantnfp1lem3  9146  infxpenlem  9442  axpowndlem3  10024  indpi  10332  fzind  12083  injresinj  13161  seqcl2  13391  seqfveq2  13395  seqshft2  13399  monoord  13403  seqsplit  13406  seqid2  13419  seqhomo  13420  seqcoll  13825  rexuzre  14715  rexico  14716  limsupbnd2  14843  rlim2lt  14857  rlim3  14858  lo1le  15011  caurcvg  15036  lcmfunsnlem1  15984  coprmprod  16008  eulerthlem2  16122  ramtlecl  16339  sylow1lem1  18726  efgsrel  18863  elcls3  21694  cncls2  21884  cnntr  21886  filssufilg  22522  ufileu  22530  alexsubALTlem3  22660  tgpt0  22730  isucn2  22891  imasdsf1olem  22986  nmoleub2lem2  23723  ovolicc2lem3  24123  dyadmbllem  24203  dvnres  24531  rlimcnp  25546  xrlimcnp  25549  ftalem2  25654  bcmono  25856  2sqlem6  26002  eupth2lems  28020  mdslmd1lem1  30105  xrge0infss  30487  subfacp1lem6  32436  cvmliftlem7  32542  cvmliftlem10  32545  ss2mcls  32819  mclsax  32820  bj-sylget  33958  bj-nfimt  33975  bj-19.21t  34102  bj-19.37im  34105  bj-spimt2  34111  mettrifi  35036  diaintclN  38198  dibintclN  38307  dihintcl  38484  mapdh9a  38929  iunrelexp0  40053  mnuop3d  40613  imbi12VD  41213  monoordxrv  41764  rexrsb  43305  smonoord  43538  ply1mulgsumlem1  44447  setrec1lem2  44798