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  1640  ax13b  2030  ax12v2  2178  axc15  2425  mo3  2562  mo4  2564  2mo  2646  sstr2OLD  3964  ssralvOLD  4029  axprlem1  5391  axprlem2  5392  axprOLD  5399  frss  5616  fvn0ssdmfun  7061  tfi  7843  nneneq  9215  wemaplem2  9554  unxpwdom2  9595  cantnfp1lem3  9687  infxpenlem  10020  axpowndlem3  10606  indpi  10914  fzind  12684  injresinj  13794  seqcl2  14028  seqfveq2  14032  seqshft2  14036  monoord  14040  seqsplit  14043  seqid2  14056  seqhomo  14057  seqcoll  14472  rexuzre  15360  rexico  15361  limsupbnd2  15488  rlim2lt  15502  rlim3  15503  lo1le  15657  caurcvg  15682  lcmfunsnlem1  16643  coprmprod  16667  eulerthlem2  16788  ramtlecl  17007  sylow1lem1  19566  efgsrel  19702  elcls3  23008  cncls2  23198  cnntr  23200  filssufilg  23836  ufileu  23844  alexsubALTlem3  23974  tgpt0  24044  isucn2  24204  imasdsf1olem  24299  nmoleub2lem2  25054  ovolicc2lem3  25459  dyadmbllem  25539  dvnres  25872  rlimcnp  26913  xrlimcnp  26916  ftalem2  27022  bcmono  27226  2sqlem6  27372  mulsproplem13  28059  mulsproplem14  28060  eupth2lems  30153  mdslmd1lem1  32240  xrge0infss  32674  subfacp1lem6  35136  cvmliftlem7  35242  cvmliftlem10  35245  ss2mcls  35519  mclsax  35520  bj-sylget  36568  bj-nfimt  36585  bj-19.21t  36716  bj-19.37im  36719  bj-spimt2  36732  mettrifi  37710  diaintclN  41006  dibintclN  41115  dihintcl  41292  mapdh9a  41737  posbezout  42042  aks6d1c6lem3  42114  fltaccoprm  42595  fltabcoprm  42597  flt4lem5  42605  cantnfresb  43280  safesnsupfiub  43372  iunrelexp0  43658  mnuop3d  44228  imbi12VD  44831  monoordxrv  45442  natlocalincr  46841  fcoresf1  47034  rexrsb  47065  smonoord  47311  ply1mulgsumlem1  48256  setrec1lem2  49393  pgindnf  49421