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  1645  ax13b  2036  ax12v2  2175  axc15  2422  mo3  2564  mo4  2566  2mo  2650  sstr2  3924  ssralv  3983  axprlem1  5341  axprlem2  5342  axpr  5346  frss  5547  fvn0ssdmfun  6934  tfi  7675  nneneq  8896  wemaplem2  9236  unxpwdom2  9277  cantnfp1lem3  9368  infxpenlem  9700  axpowndlem3  10286  indpi  10594  fzind  12348  injresinj  13436  seqcl2  13669  seqfveq2  13673  seqshft2  13677  monoord  13681  seqsplit  13684  seqid2  13697  seqhomo  13698  seqcoll  14106  rexuzre  14992  rexico  14993  limsupbnd2  15120  rlim2lt  15134  rlim3  15135  lo1le  15291  caurcvg  15316  lcmfunsnlem1  16270  coprmprod  16294  eulerthlem2  16411  ramtlecl  16629  sylow1lem1  19118  efgsrel  19255  elcls3  22142  cncls2  22332  cnntr  22334  filssufilg  22970  ufileu  22978  alexsubALTlem3  23108  tgpt0  23178  isucn2  23339  imasdsf1olem  23434  nmoleub2lem2  24185  ovolicc2lem3  24588  dyadmbllem  24668  dvnres  25000  rlimcnp  26020  xrlimcnp  26023  ftalem2  26128  bcmono  26330  2sqlem6  26476  eupth2lems  28503  mdslmd1lem1  30588  xrge0infss  30985  subfacp1lem6  33047  cvmliftlem7  33153  cvmliftlem10  33156  ss2mcls  33430  mclsax  33431  bj-sylget  34729  bj-nfimt  34746  bj-19.21t  34878  bj-19.37im  34881  bj-spimt2  34894  mettrifi  35842  diaintclN  38999  dibintclN  39108  dihintcl  39285  mapdh9a  39730  fltaccoprm  40393  fltabcoprm  40395  flt4lem5  40403  iunrelexp0  41199  mnuop3d  41778  imbi12VD  42382  monoordxrv  42912  fcoresf1  44450  rexrsb  44479  smonoord  44711  ply1mulgsumlem1  45615  setrec1lem2  46280