Theorem 3exp2 1355

Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3exp2.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
3exp2	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem 3exp2

Step	Hyp	Ref	Expression
1		3exp2.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
2	1	ex 412	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	3expd 1354	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anassrs  1361  pm2.61da3ne  3017  po2nr  5533  fliftfund  7242  frfi  9164  fin33i  10255  axdc3lem4  10339  iscatd  17574  isfuncd  17767  isposd  18223  pospropd  18226  imasmnd2  18677  grpinveu  18882  grpid  18883  grpasscan1  18909  imasgrp2  18963  dmdprdd  19908  pgpfac1lem5  19988  imasrng  20090  imasring  20243  islmodd  20794  lmodvsghm  20851  islssd  20863  islmhm2  20967  mulgghm2  21408  isphld  21586  riinopn  22818  ordtbaslem  23098  subbascn  23164  haust1  23262  isnrm2  23268  isnrm3  23269  lmmo  23290  nllyidm  23399  tx1stc  23560  filin  23764  filtop  23765  isfil2  23766  infil  23773  fgfil  23785  isufil2  23818  ufileu  23829  filufint  23830  flimopn  23885  flimrest  23893  isxmetd  24236  met2ndc  24433  icccmplem2  24734  lmmbr  25180  cfil3i  25191  equivcfil  25221  bcthlem5  25250  volfiniun  25470  dvidlem  25838  ulmdvlem3  26333  ax5seg  28911  axcontlem4  28940  axcont  28949  grporcan  30490  grpoinveu  30491  grpoid  30492  cvxpconn  35278  cvxsconn  35279  mclsax  35605  mclsppslem  35619  r1peuqusdeg1  35679  broutsideof2  36156  nn0prpwlem  36356  fgmin  36404  poimirlem27  37687  poimirlem29  37689  poimirlem31  37691  cntotbnd  37836  heiborlem6  37856  heiborlem10  37860  rngonegmn1l  37981  rngonegmn1r  37982  rngoneglmul  37983  rngonegrmul  37984  crngm23  38042  prnc  38107  pridlc3  38113  dmncan1  38116  lsmsat  39047  eqlkr  39138  llncmp  39561  2at0mat0  39564  llncvrlpln  39597  lplncmp  39601  lplnexllnN  39603  lplncvrlvol  39655  lvolcmp  39656  linepsubN  39791  pmapsub  39807  paddasslem16  39874  pmodlem2  39886  lhp2lt  40040  ltrneq2  40187  cdlemf2  40601  cdlemk34  40949  cdlemn11pre  41249  dihord2pre  41264  onexoegt  43277  clnbgrssedg  47872  clnbgrgrimlem  47964  grimgrtri  47980