Theorem 3impb 1201

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

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

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 982

This theorem is referenced by:  3adant1l  1232  3adant1r  1233  3impdi  1304  vtocl3gf  2827  rspc2ev  2883  reuss  3445  trssord  4416  funtp  5312  resdif  5529  funimass4  5614  fnovex  5958  fnotovb  5969  fovcdm  6070  fnovrn  6075  fmpoco  6283  nndi  6553  nnaordi  6575  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  eqsupti  7071  addasspig  7416  mulasspig  7418  distrpig  7419  distrnq0  7545  addassnq0  7548  distnq0r  7549  prcdnql  7570  prcunqu  7571  genpassl  7610  genpassu  7611  genpassg  7612  distrlem1prl  7668  distrlem1pru  7669  ltexprlemopl  7687  ltexprlemopu  7689  le2tri3i  8154  cnegexlem1  8220  subadd  8248  addsub  8256  subdi  8430  submul2  8444  div12ap  8740  diveqap1  8751  divnegap  8752  divdivap2  8770  ltmulgt11  8910  gt0div  8916  ge0div  8917  uzind3  9458  fnn0ind  9461  qdivcl  9736  irrmul  9740  xrlttr  9889  fzen  10137  lenegsq  11279  moddvds  11983  dvds2add  12009  dvds2sub  12010  dvdsleabs  12029  divalgb  12109  ndvdsadd  12115  modgcd  12185  absmulgcd  12211  odzval  12437  pcmul  12497  setsresg  12743  prdssgrpd  13119  issubmnd  13146  prdsmndd  13152  submcl  13183  grpinvid1  13256  grpinvid2  13257  mulgp1  13363  ghmlin  13456  ghmsub  13459  cmncom  13510  islss3  14013  unopn  14349  innei  14507  cncfi  14922