Theorem 3impb 1158

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

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

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

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

This theorem is referenced by:  3adant1l  1189  3adant1r  1190  3impdi  1252  vtocl3gf  2718  rspc2ev  2772  reuss  3321  trssord  4260  funtp  5132  resdif  5343  funimass4  5424  fnovex  5756  fnotovb  5766  fovrn  5865  fnovrn  5870  fmpoco  6064  nndi  6333  nnaordi  6355  ecovass  6489  ecoviass  6490  ecovdi  6491  ecovidi  6492  eqsupti  6832  addasspig  7079  mulasspig  7081  distrpig  7082  distrnq0  7208  addassnq0  7211  distnq0r  7212  prcdnql  7233  prcunqu  7234  genpassl  7273  genpassu  7274  genpassg  7275  distrlem1prl  7331  distrlem1pru  7332  ltexprlemopl  7350  ltexprlemopu  7352  le2tri3i  7788  cnegexlem1  7853  subadd  7881  addsub  7889  subdi  8059  submul2  8073  div12ap  8360  diveqap1  8371  divnegap  8372  divdivap2  8390  ltmulgt11  8525  gt0div  8531  ge0div  8532  uzind3  9061  fnn0ind  9064  qdivcl  9330  irrmul  9334  xrlttr  9467  fzen  9709  lenegsq  10752  moddvds  11343  dvds2add  11368  dvds2sub  11369  dvdsleabs  11384  divalgb  11463  ndvdsadd  11469  modgcd  11520  absmulgcd  11544  setsresg  11833  unopn  12008  innei  12168  cncfi  12544