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  1639  ax13b  2031  ax12v2  2180  axc15  2430  mo3  2567  mo4  2569  2mo  2651  sstr2OLD  4016  ssralvOLD  4081  axprlem1  5441  axprlem2  5442  axpr  5446  frss  5664  fvn0ssdmfun  7108  tfi  7890  nneneq  9272  nneneqOLD  9284  wemaplem2  9616  unxpwdom2  9657  cantnfp1lem3  9749  infxpenlem  10082  axpowndlem3  10668  indpi  10976  fzind  12741  injresinj  13838  seqcl2  14071  seqfveq2  14075  seqshft2  14079  monoord  14083  seqsplit  14086  seqid2  14099  seqhomo  14100  seqcoll  14513  rexuzre  15401  rexico  15402  limsupbnd2  15529  rlim2lt  15543  rlim3  15544  lo1le  15700  caurcvg  15725  lcmfunsnlem1  16684  coprmprod  16708  eulerthlem2  16829  ramtlecl  17047  sylow1lem1  19640  efgsrel  19776  elcls3  23112  cncls2  23302  cnntr  23304  filssufilg  23940  ufileu  23948  alexsubALTlem3  24078  tgpt0  24148  isucn2  24309  imasdsf1olem  24404  nmoleub2lem2  25168  ovolicc2lem3  25573  dyadmbllem  25653  dvnres  25987  rlimcnp  27026  xrlimcnp  27029  ftalem2  27135  bcmono  27339  2sqlem6  27485  mulsproplem13  28172  mulsproplem14  28173  eupth2lems  30270  mdslmd1lem1  32357  xrge0infss  32767  subfacp1lem6  35153  cvmliftlem7  35259  cvmliftlem10  35262  ss2mcls  35536  mclsax  35537  bj-sylget  36587  bj-nfimt  36604  bj-19.21t  36735  bj-19.37im  36738  bj-spimt2  36751  mettrifi  37717  diaintclN  41015  dibintclN  41124  dihintcl  41301  mapdh9a  41746  posbezout  42057  aks6d1c6lem3  42129  fltaccoprm  42595  fltabcoprm  42597  flt4lem5  42605  cantnfresb  43286  safesnsupfiub  43378  iunrelexp0  43664  mnuop3d  44240  imbi12VD  44844  monoordxrv  45397  natlocalincr  46795  fcoresf1  46984  rexrsb  47015  smonoord  47245  ply1mulgsumlem1  48115  setrec1lem2  48780  pgindnf  48808