Theorem 3impb 1199

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3adant1l  1230  3adant1r  1231  3impdi  1293  vtocl3gf  2800  rspc2ev  2856  reuss  3416  trssord  4380  funtp  5269  resdif  5483  funimass4  5566  fnovex  5907  fnotovb  5917  fovcdm  6016  fnovrn  6021  fmpoco  6216  nndi  6486  nnaordi  6508  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  eqsupti  6994  addasspig  7328  mulasspig  7330  distrpig  7331  distrnq0  7457  addassnq0  7460  distnq0r  7461  prcdnql  7482  prcunqu  7483  genpassl  7522  genpassu  7523  genpassg  7524  distrlem1prl  7580  distrlem1pru  7581  ltexprlemopl  7599  ltexprlemopu  7601  le2tri3i  8065  cnegexlem1  8131  subadd  8159  addsub  8167  subdi  8341  submul2  8355  div12ap  8650  diveqap1  8661  divnegap  8662  divdivap2  8680  ltmulgt11  8820  gt0div  8826  ge0div  8827  uzind3  9365  fnn0ind  9368  qdivcl  9642  irrmul  9646  xrlttr  9794  fzen  10042  lenegsq  11103  moddvds  11805  dvds2add  11831  dvds2sub  11832  dvdsleabs  11850  divalgb  11929  ndvdsadd  11935  modgcd  11991  absmulgcd  12017  odzval  12240  pcmul  12300  setsresg  12499  issubmnd  12842  submcl  12869  grpinvid1  12923  grpinvid2  12924  mulgp1  13014  cmncom  13103  unopn  13475  innei  13633  cncfi  14035