Theorem 3impb 1200

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 1194	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 981

This theorem is referenced by:  3adant1l  1231  3adant1r  1232  3impdi  1303  vtocl3gf  2812  rspc2ev  2868  reuss  3428  trssord  4392  funtp  5281  resdif  5495  funimass4  5579  fnovex  5921  fnotovb  5931  fovcdm  6031  fnovrn  6036  fmpoco  6231  nndi  6501  nnaordi  6523  ecovass  6658  ecoviass  6659  ecovdi  6660  ecovidi  6661  eqsupti  7009  addasspig  7343  mulasspig  7345  distrpig  7346  distrnq0  7472  addassnq0  7475  distnq0r  7476  prcdnql  7497  prcunqu  7498  genpassl  7537  genpassu  7538  genpassg  7539  distrlem1prl  7595  distrlem1pru  7596  ltexprlemopl  7614  ltexprlemopu  7616  le2tri3i  8080  cnegexlem1  8146  subadd  8174  addsub  8182  subdi  8356  submul2  8370  div12ap  8665  diveqap1  8676  divnegap  8677  divdivap2  8695  ltmulgt11  8835  gt0div  8841  ge0div  8842  uzind3  9380  fnn0ind  9383  qdivcl  9657  irrmul  9661  xrlttr  9809  fzen  10057  lenegsq  11118  moddvds  11820  dvds2add  11846  dvds2sub  11847  dvdsleabs  11865  divalgb  11944  ndvdsadd  11950  modgcd  12006  absmulgcd  12032  odzval  12255  pcmul  12315  setsresg  12514  issubmnd  12865  submcl  12892  grpinvid1  12949  grpinvid2  12950  mulgp1  13048  cmncom  13139  islss3  13568  unopn  13801  innei  13959  cncfi  14361