Theorem 3impb 1226

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

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

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 1007

This theorem is referenced by:  3adant1l  1257  3adant1r  1258  3impdi  1330  vtocl3gf  2868  rspc2ev  2926  reuss  3490  trssord  4483  funtp  5390  resdif  5614  funimass4  5705  fnovex  6061  fnotovb  6074  fovcdm  6175  fnovrn  6180  fmpoco  6390  nndi  6697  nnaordi  6719  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  eqsupti  7238  addasspig  7593  mulasspig  7595  distrpig  7596  distrnq0  7722  addassnq0  7725  distnq0r  7726  prcdnql  7747  prcunqu  7748  genpassl  7787  genpassu  7788  genpassg  7789  distrlem1prl  7845  distrlem1pru  7846  ltexprlemopl  7864  ltexprlemopu  7866  le2tri3i  8330  cnegexlem1  8396  subadd  8424  addsub  8432  subdi  8606  submul2  8620  div12ap  8916  diveqap1  8927  divnegap  8928  divdivap2  8946  ltmulgt11  9086  gt0div  9092  ge0div  9093  uzind3  9637  fnn0ind  9640  qdivcl  9921  irrmul  9925  xrlttr  10074  fzen  10323  ccatval21sw  11231  lswccatn0lsw  11237  swrdwrdsymbg  11294  ccatpfx  11331  ccatopth  11346  lenegsq  11718  moddvds  12423  dvds2add  12449  dvds2sub  12450  dvdsleabs  12469  divalgb  12549  ndvdsadd  12555  modgcd  12625  absmulgcd  12651  odzval  12877  pcmul  12937  setsresg  13183  prdssgrpd  13561  issubmnd  13588  prdsmndd  13594  submcl  13625  grpinvid1  13698  grpinvid2  13699  mulgp1  13805  ghmlin  13898  ghmsub  13901  cmncom  13952  islss3  14458  unopn  14799  innei  14957  cncfi  15372