Theorem 3exp2 1277

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anassrs  1282  pm2.61da3ne  2871  po2nr  4972  predpo  5615  fliftfund  6463  frfi  8090  fin33i  9074  axdc3lem4  9158  relexpaddd  13642  iscatd  16157  isfuncd  16348  isposd  16778  pospropd  16957  imasmnd2  17150  grpinveu  17279  grpid  17280  grpasscan1  17301  imasgrp2  17353  dmdprdd  18221  pgpfac1lem5  18301  imasring  18442  islmodd  18692  lmodvsghm  18747  islssd  18757  islmhm2  18859  psrbaglefi  19193  mulgghm2  19664  isphld  19818  riinopn  20538  ordtbaslem  20802  subbascn  20868  haust1  20966  isnrm2  20972  isnrm3  20973  lmmo  20994  nllyidm  21102  tx1stc  21263  filin  21468  filtop  21469  isfil2  21470  infil  21477  fgfil  21489  isufil2  21522  ufileu  21533  filufint  21534  flimopn  21589  flimrest  21597  isxmetd  21941  met2ndc  22138  icccmplem2  22434  lmmbr  22864  cfil3i  22875  equivcfil  22905  bcthlem5  22933  volfiniun  23122  dvidlem  23485  ulmdvlem3  23960  ax5seg  25618  axcontlem4  25647  axcont  25656  grporcan  26756  grpoinveu  26757  grpoid  26758  cvxpcon  30478  cvxscon  30479  mclsax  30720  mclsppslem  30734  broutsideof2  31399  nn0prpwlem  31487  fgmin  31535  poimirlem27  32606  poimirlem29  32608  poimirlem31  32610  cntotbnd  32765  heiborlem6  32785  heiborlem10  32789  rngonegmn1l  32910  rngonegmn1r  32911  rngoneglmul  32912  rngonegrmul  32913  crngm23  32971  prnc  33036  pridlc3  33042  dmncan1  33045  lsmsat  33313  eqlkr  33404  llncmp  33826  2at0mat0  33829  llncvrlpln  33862  lplncmp  33866  lplnexllnN  33868  lplncvrlvol  33920  lvolcmp  33921  linepsubN  34056  pmapsub  34072  paddasslem16  34139  pmodlem2  34151  lhp2lt  34305  ltrneq2  34452  cdlemf2  34868  cdlemk34  35216  cdlemn11pre  35517  dihord2pre  35532