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  342  meredith  1644  ax13b  2036  ax12v2  2174  axc15  2423  mo3  2565  mo4  2567  2mo  2651  sstr2  3929  ssralv  3988  axprlem1  5347  axprlem2  5348  axpr  5352  frss  5557  fvn0ssdmfun  6961  tfi  7709  nneneq  9001  nneneqOLD  9013  wemaplem2  9315  unxpwdom2  9356  cantnfp1lem3  9447  infxpenlem  9778  axpowndlem3  10364  indpi  10672  fzind  12427  injresinj  13517  seqcl2  13750  seqfveq2  13754  seqshft2  13758  monoord  13762  seqsplit  13765  seqid2  13778  seqhomo  13779  seqcoll  14187  rexuzre  15073  rexico  15074  limsupbnd2  15201  rlim2lt  15215  rlim3  15216  lo1le  15372  caurcvg  15397  lcmfunsnlem1  16351  coprmprod  16375  eulerthlem2  16492  ramtlecl  16710  sylow1lem1  19212  efgsrel  19349  elcls3  22243  cncls2  22433  cnntr  22435  filssufilg  23071  ufileu  23079  alexsubALTlem3  23209  tgpt0  23279  isucn2  23440  imasdsf1olem  23535  nmoleub2lem2  24288  ovolicc2lem3  24692  dyadmbllem  24772  dvnres  25104  rlimcnp  26124  xrlimcnp  26127  ftalem2  26232  bcmono  26434  2sqlem6  26580  eupth2lems  28611  mdslmd1lem1  30696  xrge0infss  31092  subfacp1lem6  33156  cvmliftlem7  33262  cvmliftlem10  33265  ss2mcls  33539  mclsax  33540  bj-sylget  34811  bj-nfimt  34828  bj-19.21t  34960  bj-19.37im  34963  bj-spimt2  34976  mettrifi  35924  diaintclN  39079  dibintclN  39188  dihintcl  39365  mapdh9a  39810  fltaccoprm  40484  fltabcoprm  40486  flt4lem5  40494  iunrelexp0  41317  mnuop3d  41896  imbi12VD  42500  monoordxrv  43029  fcoresf1  44574  rexrsb  44603  smonoord  44834  ply1mulgsumlem1  45738  setrec1lem2  46405  natlocalincr  46522