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  343  meredith  1651  ax13b  2042  ax12v2  2204  axc15  2443  mo3  2581  mo4  2583  2mo  2665  axprlem2  5371  axprlem1OLD  5375  axprOLD  5379  axprglem  5383  frss  5600  fvn0ssdmfun  7040  tfi  7818  nneneq  9159  wemaplem2  9481  unxpwdom2  9522  cantnfp1lem3  9621  infxpenlem  9955  axpowndlem3  10543  indpi  10851  fzind  12657  injresinj  13783  seqcl2  14019  seqfveq2  14023  seqshft2  14027  monoord  14031  seqsplit  14034  seqid2  14047  seqhomo  14048  seqcoll  14463  rexuzre  15352  rexico  15353  limsupbnd2  15482  rlim2lt  15496  rlim3  15497  lo1le  15651  caurcvg  15676  lcmfunsnlem1  16643  coprmprod  16667  eulerthlem2  16789  ramtlecl  17008  sylow1lem1  19610  efgsrel  19746  elcls3  23112  cncls2  23302  cnntr  23304  filssufilg  23940  ufileu  23948  alexsubALTlem3  24078  tgpt0  24148  isucn2  24307  imasdsf1olem  24402  nmoleub2lem2  25147  ovolicc2lem3  25550  dyadmbllem  25630  dvnres  25962  rlimcnp  26996  xrlimcnp  26999  ftalem2  27104  bcmono  27307  2sqlem6  27453  mulsproplem13  28187  mulsproplem14  28188  eupth2lems  30375  mdslmd1lem1  32463  xrge0infss  32901  axpowg2  35388  axpowg3  35389  subfacp1lem6  35473  cvmliftlem7  35579  cvmliftlem10  35582  ss2mcls  35856  mclsax  35857  axtco2  36772  bj-imim11  36929  bj-sylget  37014  bj-19.21t  37174  bj-spimt2  37208  mettrifi  38194  diaintclN  41620  dibintclN  41729  dihintcl  41906  mapdh9a  42351  posbezout  42655  aks6d1c6lem3  42727  fltaccoprm  43160  fltabcoprm  43162  flt4lem5  43170  cantnfresb  43839  safesnsupfiub  43930  iunrelexp0  44216  mnuop3d  44785  imbi12VD  45386  monoordxrv  45993  natlocalincr  47390  fcoresf1  47601  rexrsb  47632  smonoord  47909  ply1mulgsumlem1  48946  setrec1lem2  50247  pgindnf  50275