Theorem 3exp2 1373

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 418	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	3expd 1372	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anassrs  1381  pm2.61da3ne  3045  po2nr  5573  fliftfund  7319  frfi  9269  fin33i  10440  axdc3lem4  10524  iscatd  17840  isfuncd  18033  isposd  18489  pospropd  18492  imasmnd2  18961  grpinveu  19178  grpid  19179  grpasscan1  19205  imasgrp2  19258  dmdprdd  20208  pgpfac1lem5  20288  imasrng  20392  imasring  20553  islmodd  21134  lmodvsghm  21191  islssd  21203  islmhm2  21306  cmprmidlmcl  21624  mulgghm2  21775  isphld  21953  riinopn  23219  ordtbaslem  23499  subbascn  23565  haust1  23663  isnrm2  23669  isnrm3  23670  lmmo  23691  nllyidm  23801  tx1stc  23962  filin  24166  filtop  24167  isfil2  24168  infil  24175  fgfil  24187  isufil2  24220  ufileu  24231  filufint  24232  flimopn  24287  flimrest  24295  isxmetd  24638  met2ndc  24835  icccmplem2  25136  lmmbr  25572  cfil3i  25583  equivcfil  25613  bcthlem5  25642  volfiniun  25861  dvidlem  26228  ulmdvlem3  26722  ax5seg  29509  axcontlem4  29538  axcont  29547  grporcan  31113  grpoinveu  31114  grpoid  31115  cvxpconn  35986  cvxsconn  35987  mclsax  36313  mclsppslem  36327  r1peuqusdeg1  36387  broutsideof2  36867  nn0prpwlem  37090  fgmin  37138  poimirlem27  38545  poimirlem29  38547  poimirlem31  38549  cntotbnd  38710  heiborlem6  38730  heiborlem10  38734  rngonegmn1l  38855  rngonegmn1r  38856  rngoneglmul  38857  rngonegrmul  38858  crngm23  38916  prnc  38981  pridlc3  38987  dmncan1  38990  lsmsat  40045  eqlkr  40136  llncmp  40559  2at0mat0  40562  llncvrlpln  40595  lplncmp  40599  lplnexllnN  40601  lplncvrlvol  40653  lvolcmp  40654  linepsubN  40789  pmapsub  40805  paddasslem16  40872  pmodlem2  40884  lhp2lt  41038  ltrneq2  41185  cdlemf2  41599  cdlemk34  41947  cdlemn11pre  42247  dihord2pre  42262  onexoegt  44230  clnbgrssedg  48908  clnbgrgrimlem  49000  grimgrtri  49016  idomcanl  49413