Theorem 3impb 1188

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 967

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

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  3adant1l  1219  3adant1r  1220  3impdi  1282  vtocl3gf  2784  rspc2ev  2840  reuss  3398  trssord  4352  funtp  5235  resdif  5448  funimass4  5531  fnovex  5866  fnotovb  5876  fovrn  5975  fnovrn  5980  fmpoco  6175  nndi  6445  nnaordi  6467  ecovass  6601  ecoviass  6602  ecovdi  6603  ecovidi  6604  eqsupti  6952  addasspig  7262  mulasspig  7264  distrpig  7265  distrnq0  7391  addassnq0  7394  distnq0r  7395  prcdnql  7416  prcunqu  7417  genpassl  7456  genpassu  7457  genpassg  7458  distrlem1prl  7514  distrlem1pru  7515  ltexprlemopl  7533  ltexprlemopu  7535  le2tri3i  7998  cnegexlem1  8064  subadd  8092  addsub  8100  subdi  8274  submul2  8288  div12ap  8581  diveqap1  8592  divnegap  8593  divdivap2  8611  ltmulgt11  8750  gt0div  8756  ge0div  8757  uzind3  9295  fnn0ind  9298  qdivcl  9572  irrmul  9576  xrlttr  9722  fzen  9968  lenegsq  11023  moddvds  11725  dvds2add  11751  dvds2sub  11752  dvdsleabs  11768  divalgb  11847  ndvdsadd  11853  modgcd  11909  absmulgcd  11935  odzval  12150  pcmul  12210  setsresg  12369  unopn  12544  innei  12704  cncfi  13106