Theorem 3impb 1100

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 347	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1098	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3adant1l  1127  3adant1r  1128  3impdi  1190  vtocl3gf  2616  rspc2ev  2664  reuss  3218  trssord  4117  funtp  4952  resdif  5148  funimass4  5224  fnovex  5538  fnotovb  5548  fovrn  5643  fnovrn  5648  fmpt2co  5837  nndi  6065  nnaordi  6081  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addasspig  6428  mulasspig  6430  distrpig  6431  distrnq0  6557  addassnq0  6560  distnq0r  6561  prcdnql  6582  prcunqu  6583  genpassl  6622  genpassu  6623  genpassg  6624  distrlem1prl  6680  distrlem1pru  6681  ltexprlemopl  6699  ltexprlemopu  6701  le2tri3i  7126  cnegexlem1  7186  subadd  7214  addsub  7222  subdi  7382  submul2  7396  div12ap  7673  diveqap1  7682  divnegap  7683  divdivap2  7700  ltmulgt11  7830  gt0div  7836  ge0div  7837  uzind3  8351  fnn0ind  8354  qdivcl  8577  irrmul  8581  xrlttr  8716  fzen  8907  iseqval  9220  lenegsq  9691