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  exptOLD  178  imbi1d  342  meredith  1648  ax13b  2039  ax12v2  2191  axc15  2430  mo3  2568  mo4  2570  2mo  2652  axprlem2  5360  axprlem1OLD  5364  axprOLD  5368  axprglem  5372  frss  5589  fvn0ssdmfun  7022  tfi  7800  nneneq  9137  wemaplem2  9459  unxpwdom2  9500  cantnfp1lem3  9599  infxpenlem  9933  axpowndlem3  10520  indpi  10828  fzind  12625  injresinj  13744  seqcl2  13980  seqfveq2  13984  seqshft2  13988  monoord  13992  seqsplit  13995  seqid2  14008  seqhomo  14009  seqcoll  14424  rexuzre  15313  rexico  15314  limsupbnd2  15443  rlim2lt  15457  rlim3  15458  lo1le  15612  caurcvg  15637  lcmfunsnlem1  16604  coprmprod  16628  eulerthlem2  16750  ramtlecl  16969  sylow1lem1  19571  efgsrel  19707  elcls3  23073  cncls2  23263  cnntr  23265  filssufilg  23901  ufileu  23909  alexsubALTlem3  24039  tgpt0  24109  isucn2  24268  imasdsf1olem  24363  nmoleub2lem2  25108  ovolicc2lem3  25511  dyadmbllem  25591  dvnres  25923  rlimcnp  26954  xrlimcnp  26957  ftalem2  27062  bcmono  27265  2sqlem6  27411  mulsproplem13  28145  mulsproplem14  28146  eupth2lems  30333  mdslmd1lem1  32421  xrge0infss  32859  axpowg2  35335  axpowg3  35336  subfacp1lem6  35420  cvmliftlem7  35526  cvmliftlem10  35529  ss2mcls  35803  mclsax  35804  axtco2  36709  bj-imim11  36866  bj-sylget  36951  bj-19.21t  37111  bj-spimt2  37145  mettrifi  38131  diaintclN  41557  dibintclN  41666  dihintcl  41843  mapdh9a  42288  posbezout  42592  aks6d1c6lem3  42664  fltaccoprm  43097  fltabcoprm  43099  flt4lem5  43107  cantnfresb  43776  safesnsupfiub  43867  iunrelexp0  44153  mnuop3d  44722  imbi12VD  45323  monoordxrv  45931  natlocalincr  47328  fcoresf1  47539  rexrsb  47570  smonoord  47847  ply1mulgsumlem1  48884  setrec1lem2  50185  pgindnf  50213