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  3021  po2nr  5575  fliftfund  7306  frfi  9293  fin33i  10383  axdc3lem4  10467  iscatd  17685  isfuncd  17878  isposd  18334  pospropd  18337  imasmnd2  18752  grpinveu  18957  grpid  18958  grpasscan1  18984  imasgrp2  19038  dmdprdd  19982  pgpfac1lem5  20062  imasrng  20137  imasring  20290  islmodd  20823  lmodvsghm  20880  islssd  20892  islmhm2  20996  mulgghm2  21437  isphld  21614  riinopn  22846  ordtbaslem  23126  subbascn  23192  haust1  23290  isnrm2  23296  isnrm3  23297  lmmo  23318  nllyidm  23427  tx1stc  23588  filin  23792  filtop  23793  isfil2  23794  infil  23801  fgfil  23813  isufil2  23846  ufileu  23857  filufint  23858  flimopn  23913  flimrest  23921  isxmetd  24265  met2ndc  24462  icccmplem2  24763  lmmbr  25210  cfil3i  25221  equivcfil  25251  bcthlem5  25280  volfiniun  25500  dvidlem  25868  ulmdvlem3  26363  ax5seg  28917  axcontlem4  28946  axcont  28955  grporcan  30499  grpoinveu  30500  grpoid  30501  cvxpconn  35264  cvxsconn  35265  mclsax  35591  mclsppslem  35605  r1peuqusdeg1  35665  broutsideof2  36140  nn0prpwlem  36340  fgmin  36388  poimirlem27  37671  poimirlem29  37673  poimirlem31  37675  cntotbnd  37820  heiborlem6  37840  heiborlem10  37844  rngonegmn1l  37965  rngonegmn1r  37966  rngoneglmul  37967  rngonegrmul  37968  crngm23  38026  prnc  38091  pridlc3  38097  dmncan1  38100  lsmsat  39026  eqlkr  39117  llncmp  39541  2at0mat0  39544  llncvrlpln  39577  lplncmp  39581  lplnexllnN  39583  lplncvrlvol  39635  lvolcmp  39636  linepsubN  39771  pmapsub  39787  paddasslem16  39854  pmodlem2  39866  lhp2lt  40020  ltrneq2  40167  cdlemf2  40581  cdlemk34  40929  cdlemn11pre  41229  dihord2pre  41244  onexoegt  43268  clnbgrssedg  47854  clnbgrgrimlem  47946  grimgrtri  47961