Theorem 3impb 1225

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

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

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 1006

This theorem is referenced by:  3adant1l  1256  3adant1r  1257  3impdi  1329  vtocl3gf  2867  rspc2ev  2925  reuss  3488  trssord  4477  funtp  5383  resdif  5605  funimass4  5696  fnovex  6050  fnotovb  6063  fovcdm  6164  fnovrn  6169  fmpoco  6380  nndi  6653  nnaordi  6675  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  eqsupti  7194  addasspig  7549  mulasspig  7551  distrpig  7552  distrnq0  7678  addassnq0  7681  distnq0r  7682  prcdnql  7703  prcunqu  7704  genpassl  7743  genpassu  7744  genpassg  7745  distrlem1prl  7801  distrlem1pru  7802  ltexprlemopl  7820  ltexprlemopu  7822  le2tri3i  8287  cnegexlem1  8353  subadd  8381  addsub  8389  subdi  8563  submul2  8577  div12ap  8873  diveqap1  8884  divnegap  8885  divdivap2  8903  ltmulgt11  9043  gt0div  9049  ge0div  9050  uzind3  9592  fnn0ind  9595  qdivcl  9876  irrmul  9880  xrlttr  10029  fzen  10277  ccatval21sw  11181  lswccatn0lsw  11187  swrdwrdsymbg  11244  ccatpfx  11281  ccatopth  11296  lenegsq  11655  moddvds  12359  dvds2add  12385  dvds2sub  12386  dvdsleabs  12405  divalgb  12485  ndvdsadd  12491  modgcd  12561  absmulgcd  12587  odzval  12813  pcmul  12873  setsresg  13119  prdssgrpd  13497  issubmnd  13524  prdsmndd  13530  submcl  13561  grpinvid1  13634  grpinvid2  13635  mulgp1  13741  ghmlin  13834  ghmsub  13837  cmncom  13888  islss3  14392  unopn  14728  innei  14886  cncfi  15301