Theorem 3impb 1135

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impb.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3impb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 357	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1133	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3adant1l  1162  3adant1r  1163  3impdi  1225  vtocl3gf  2672  rspc2ev  2725  reuss  3263  trssord  4171  funtp  5020  resdif  5223  funimass4  5300  fnovex  5617  fnotovb  5627  fovrn  5722  fnovrn  5727  fmpt2co  5916  nndi  6179  nnaordi  6197  ecovass  6331  ecoviass  6332  ecovdi  6333  ecovidi  6334  eqsupti  6598  addasspig  6792  mulasspig  6794  distrpig  6795  distrnq0  6921  addassnq0  6924  distnq0r  6925  prcdnql  6946  prcunqu  6947  genpassl  6986  genpassu  6987  genpassg  6988  distrlem1prl  7044  distrlem1pru  7045  ltexprlemopl  7063  ltexprlemopu  7065  le2tri3i  7496  cnegexlem1  7560  subadd  7588  addsub  7596  subdi  7766  submul2  7780  div12ap  8059  diveqap1  8070  divnegap  8071  divdivap2  8089  ltmulgt11  8219  gt0div  8225  ge0div  8226  uzind3  8755  fnn0ind  8758  qdivcl  9023  irrmul  9027  xrlttr  9160  fzen  9352  iseqval  9749  lenegsq  10355  moddvds  10585  dvds2add  10610  dvds2sub  10611  dvdsleabs  10626  divalgb  10705  ndvdsadd  10711  modgcd  10762  absmulgcd  10786