Theorem imim1d 83

Description: Deduction adding nested consequents. Deduction associated with imim1 84 and imim1i 64. (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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	imim12d 82	1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1  84  exptOLD  179  imbi1d  344  meredith  1674  ax13b  2065  ax12v2  2215  axc15  2452  mo3  2590  mo4  2592  2mo  2674  axprlem2  5386  axprlem1OLD  5390  axprglem  5394  frss  5615  fvn0ssdmfun  7066  tfi  7853  nneneq  9205  wemaplem2  9525  unxpwdom2  9566  cantnfp1lem3  9665  setrec1lem2  9948  infxpenlem  10073  axpowndlem3  10665  indpi  10973  fzind  12778  injresinj  13906  seqcl2  14143  seqfveq2  14147  seqshft2  14151  monoord  14155  seqsplit  14158  seqid2  14171  seqhomo  14172  seqcoll  14589  rexuzre  15500  rexico  15501  limsupbnd2  15630  rlim2lt  15644  rlim3  15645  lo1le  15799  caurcvg  15824  lcmfunsnlem1  16792  coprmprod  16816  eulerthlem2  16939  ramtlecl  17158  sylow1lem1  19792  efgsrel  19928  elcls3  23381  cncls2  23571  cnntr  23573  filssufilg  24210  ufileu  24218  alexsubALTlem3  24348  tgpt0  24418  isucn2  24577  imasdsf1olem  24672  nmoleub2lem2  25417  ovolicc2lem3  25820  dyadmbllem  25900  dvnres  26231  rlimcnp  27275  xrlimcnp  27278  ftalem2  27383  bcmono  27586  2sqlem6  27732  fltaccoprm  27954  fltabcoprm  27956  flt4lem5  27962  mulsproplem13  28496  mulsproplem14  28497  eupth2lems  30821  mdslmd1lem1  32909  xrge0infss  33334  axpowg2  35788  axpowg3  35789  subfacp1lem6  35919  cvmliftlem7  36025  cvmliftlem10  36028  ss2mcls  36302  mclsax  36303  axtco2  37232  bj-imim11  37388  bj-sylget  37473  bj-19.21t  37633  bj-spimt2  37667  findcard4  38600  mettrifi  38659  diaintclN  42083  dibintclN  42192  dihintcl  42369  mapdh9a  42814  posbezout  43118  aks6d1c6lem3  43190  cantnfresb  44284  safesnsupfiub  44375  iunrelexp0  44661  mnuop3d  45214  imbi12VD  45814  monoordxrv  46435  fcoresf1  48083  rexrsb  48114  smonoord  48391  ply1mulgsumlem1  49442  pgindnf  50753