Theorem 3exp2 1356

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 1355	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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

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 1089

This theorem is referenced by:  3anassrs  1362  pm2.61da3ne  3021  po2nr  5553  fliftfund  7268  frfi  9195  fin33i  10291  axdc3lem4  10375  iscatd  17639  isfuncd  17832  isposd  18288  pospropd  18291  imasmnd2  18742  grpinveu  18950  grpid  18951  grpasscan1  18977  imasgrp2  19031  dmdprdd  19976  pgpfac1lem5  20056  imasrng  20158  imasring  20310  islmodd  20861  lmodvsghm  20918  islssd  20930  islmhm2  21033  mulgghm2  21456  isphld  21634  riinopn  22873  ordtbaslem  23153  subbascn  23219  haust1  23317  isnrm2  23323  isnrm3  23324  lmmo  23345  nllyidm  23454  tx1stc  23615  filin  23819  filtop  23820  isfil2  23821  infil  23828  fgfil  23840  isufil2  23873  ufileu  23884  filufint  23885  flimopn  23940  flimrest  23948  isxmetd  24291  met2ndc  24488  icccmplem2  24789  lmmbr  25225  cfil3i  25236  equivcfil  25266  bcthlem5  25295  volfiniun  25514  dvidlem  25882  ulmdvlem3  26367  ax5seg  29007  axcontlem4  29036  axcont  29045  grporcan  30589  grpoinveu  30590  grpoid  30591  cvxpconn  35424  cvxsconn  35425  mclsax  35751  mclsppslem  35765  r1peuqusdeg1  35825  broutsideof2  36304  nn0prpwlem  36504  fgmin  36552  poimirlem27  37968  poimirlem29  37970  poimirlem31  37972  cntotbnd  38117  heiborlem6  38137  heiborlem10  38141  rngonegmn1l  38262  rngonegmn1r  38263  rngoneglmul  38264  rngonegrmul  38265  crngm23  38323  prnc  38388  pridlc3  38394  dmncan1  38397  lsmsat  39454  eqlkr  39545  llncmp  39968  2at0mat0  39971  llncvrlpln  40004  lplncmp  40008  lplnexllnN  40010  lplncvrlvol  40062  lvolcmp  40063  linepsubN  40198  pmapsub  40214  paddasslem16  40281  pmodlem2  40293  lhp2lt  40447  ltrneq2  40594  cdlemf2  41008  cdlemk34  41356  cdlemn11pre  41656  dihord2pre  41671  onexoegt  43672  clnbgrssedg  48317  clnbgrgrimlem  48409  grimgrtri  48425