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  3014  po2nr  5560  fliftfund  7288  frfi  9232  fin33i  10322  axdc3lem4  10406  iscatd  17634  isfuncd  17827  isposd  18283  pospropd  18286  imasmnd2  18701  grpinveu  18906  grpid  18907  grpasscan1  18933  imasgrp2  18987  dmdprdd  19931  pgpfac1lem5  20011  imasrng  20086  imasring  20239  islmodd  20772  lmodvsghm  20829  islssd  20841  islmhm2  20945  mulgghm2  21386  isphld  21563  riinopn  22795  ordtbaslem  23075  subbascn  23141  haust1  23239  isnrm2  23245  isnrm3  23246  lmmo  23267  nllyidm  23376  tx1stc  23537  filin  23741  filtop  23742  isfil2  23743  infil  23750  fgfil  23762  isufil2  23795  ufileu  23806  filufint  23807  flimopn  23862  flimrest  23870  isxmetd  24214  met2ndc  24411  icccmplem2  24712  lmmbr  25158  cfil3i  25169  equivcfil  25199  bcthlem5  25228  volfiniun  25448  dvidlem  25816  ulmdvlem3  26311  ax5seg  28865  axcontlem4  28894  axcont  28903  grporcan  30447  grpoinveu  30448  grpoid  30449  cvxpconn  35229  cvxsconn  35230  mclsax  35556  mclsppslem  35570  r1peuqusdeg1  35630  broutsideof2  36110  nn0prpwlem  36310  fgmin  36358  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  cntotbnd  37790  heiborlem6  37810  heiborlem10  37814  rngonegmn1l  37935  rngonegmn1r  37936  rngoneglmul  37937  rngonegrmul  37938  crngm23  37996  prnc  38061  pridlc3  38067  dmncan1  38070  lsmsat  39001  eqlkr  39092  llncmp  39516  2at0mat0  39519  llncvrlpln  39552  lplncmp  39556  lplnexllnN  39558  lplncvrlvol  39610  lvolcmp  39611  linepsubN  39746  pmapsub  39762  paddasslem16  39829  pmodlem2  39841  lhp2lt  39995  ltrneq2  40142  cdlemf2  40556  cdlemk34  40904  cdlemn11pre  41204  dihord2pre  41219  onexoegt  43233  clnbgrssedg  47841  clnbgrgrimlem  47933  grimgrtri  47948