Theorem 3impb 1177

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

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

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 964

This theorem is referenced by:  3adant1l  1208  3adant1r  1209  3impdi  1271  vtocl3gf  2749  rspc2ev  2804  reuss  3357  trssord  4302  funtp  5176  resdif  5389  funimass4  5472  fnovex  5804  fnotovb  5814  fovrn  5913  fnovrn  5918  fmpoco  6113  nndi  6382  nnaordi  6404  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  eqsupti  6883  addasspig  7138  mulasspig  7140  distrpig  7141  distrnq0  7267  addassnq0  7270  distnq0r  7271  prcdnql  7292  prcunqu  7293  genpassl  7332  genpassu  7333  genpassg  7334  distrlem1prl  7390  distrlem1pru  7391  ltexprlemopl  7409  ltexprlemopu  7411  le2tri3i  7872  cnegexlem1  7937  subadd  7965  addsub  7973  subdi  8147  submul2  8161  div12ap  8454  diveqap1  8465  divnegap  8466  divdivap2  8484  ltmulgt11  8622  gt0div  8628  ge0div  8629  uzind3  9164  fnn0ind  9167  qdivcl  9435  irrmul  9439  xrlttr  9581  fzen  9823  lenegsq  10867  moddvds  11502  dvds2add  11527  dvds2sub  11528  dvdsleabs  11543  divalgb  11622  ndvdsadd  11628  modgcd  11679  absmulgcd  11705  setsresg  11997  unopn  12172  innei  12332  cncfi  12734