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  1642  ax13b  2033  ax12v2  2186  axc15  2426  mo3  2564  mo4  2566  2mo  2648  sstr2OLD  3941  ssralvOLD  4006  axprlem1  5368  axprlem2  5369  axprOLD  5376  frss  5588  fvn0ssdmfun  7019  tfi  7795  nneneq  9130  wemaplem2  9452  unxpwdom2  9493  cantnfp1lem3  9589  infxpenlem  9923  axpowndlem3  10510  indpi  10818  fzind  12590  injresinj  13707  seqcl2  13943  seqfveq2  13947  seqshft2  13951  monoord  13955  seqsplit  13958  seqid2  13971  seqhomo  13972  seqcoll  14387  rexuzre  15276  rexico  15277  limsupbnd2  15406  rlim2lt  15420  rlim3  15421  lo1le  15575  caurcvg  15600  lcmfunsnlem1  16564  coprmprod  16588  eulerthlem2  16709  ramtlecl  16928  sylow1lem1  19527  efgsrel  19663  elcls3  23027  cncls2  23217  cnntr  23219  filssufilg  23855  ufileu  23863  alexsubALTlem3  23993  tgpt0  24063  isucn2  24222  imasdsf1olem  24317  nmoleub2lem2  25072  ovolicc2lem3  25476  dyadmbllem  25556  dvnres  25889  rlimcnp  26931  xrlimcnp  26934  ftalem2  27040  bcmono  27244  2sqlem6  27390  mulsproplem13  28124  mulsproplem14  28125  eupth2lems  30313  mdslmd1lem1  32400  xrge0infss  32840  subfacp1lem6  35379  cvmliftlem7  35485  cvmliftlem10  35488  ss2mcls  35762  mclsax  35763  bj-sylget  36821  bj-nfimt  36838  bj-19.21t  36970  bj-19.37im  36973  bj-spimt2  36986  mettrifi  37958  diaintclN  41318  dibintclN  41427  dihintcl  41604  mapdh9a  42049  posbezout  42354  aks6d1c6lem3  42426  fltaccoprm  42883  fltabcoprm  42885  flt4lem5  42893  cantnfresb  43566  safesnsupfiub  43657  iunrelexp0  43943  mnuop3d  44512  imbi12VD  45113  monoordxrv  45725  natlocalincr  47120  fcoresf1  47315  rexrsb  47346  smonoord  47617  ply1mulgsumlem1  48632  setrec1lem2  49933  pgindnf  49961