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  340  meredith  1635  ax13b  2027  ax12v2  2168  axc15  2415  mo3  2552  mo4  2554  2mo  2636  sstr2OLD  3984  ssralvOLD  4049  axprlem1  5423  axprlem2  5424  axpr  5428  frss  5645  fvn0ssdmfun  7083  tfi  7858  nneneq  9237  nneneqOLD  9249  wemaplem2  9577  unxpwdom2  9618  cantnfp1lem3  9710  infxpenlem  10043  axpowndlem3  10629  indpi  10937  fzind  12698  injresinj  13794  seqcl2  14026  seqfveq2  14030  seqshft2  14034  monoord  14038  seqsplit  14041  seqid2  14054  seqhomo  14055  seqcoll  14469  rexuzre  15343  rexico  15344  limsupbnd2  15471  rlim2lt  15485  rlim3  15486  lo1le  15642  caurcvg  15667  lcmfunsnlem1  16624  coprmprod  16648  eulerthlem2  16770  ramtlecl  16988  sylow1lem1  19582  efgsrel  19718  elcls3  23048  cncls2  23238  cnntr  23240  filssufilg  23876  ufileu  23884  alexsubALTlem3  24014  tgpt0  24084  isucn2  24245  imasdsf1olem  24340  nmoleub2lem2  25104  ovolicc2lem3  25509  dyadmbllem  25589  dvnres  25922  rlimcnp  26962  xrlimcnp  26965  ftalem2  27071  bcmono  27275  2sqlem6  27421  mulsproplem13  28098  mulsproplem14  28099  eupth2lems  30140  mdslmd1lem1  32227  xrge0infss  32632  subfacp1lem6  34946  cvmliftlem7  35052  cvmliftlem10  35055  ss2mcls  35329  mclsax  35330  bj-sylget  36248  bj-nfimt  36265  bj-19.21t  36397  bj-19.37im  36400  bj-spimt2  36413  mettrifi  37381  diaintclN  40681  dibintclN  40790  dihintcl  40967  mapdh9a  41412  posbezout  41722  aks6d1c6lem3  41794  fltaccoprm  42204  fltabcoprm  42206  flt4lem5  42214  cantnfresb  42900  safesnsupfiub  42993  iunrelexp0  43279  mnuop3d  43855  imbi12VD  44459  monoordxrv  45007  natlocalincr  46405  fcoresf1  46594  rexrsb  46623  smonoord  46853  ply1mulgsumlem1  47645  setrec1lem2  48310  pgindnf  48338