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  2823  rspc2ev  2879  reuss  3440  trssord  4411  funtp  5307  resdif  5522  funimass4  5607  fnovex  5951  fnotovb  5961  fovcdm  6061  fnovrn  6066  fmpoco  6269  nndi  6539  nnaordi  6561  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  eqsupti  7055  addasspig  7390  mulasspig  7392  distrpig  7393  distrnq0  7519  addassnq0  7522  distnq0r  7523  prcdnql  7544  prcunqu  7545  genpassl  7584  genpassu  7585  genpassg  7586  distrlem1prl  7642  distrlem1pru  7643  ltexprlemopl  7661  ltexprlemopu  7663  le2tri3i  8128  cnegexlem1  8194  subadd  8222  addsub  8230  subdi  8404  submul2  8418  div12ap  8713  diveqap1  8724  divnegap  8725  divdivap2  8743  ltmulgt11  8883  gt0div  8889  ge0div  8890  uzind3  9430  fnn0ind  9433  qdivcl  9708  irrmul  9712  xrlttr  9861  fzen  10109  lenegsq  11239  moddvds  11942  dvds2add  11968  dvds2sub  11969  dvdsleabs  11987  divalgb  12066  ndvdsadd  12072  modgcd  12128  absmulgcd  12154  odzval  12379  pcmul  12439  setsresg  12656  issubmnd  13023  submcl  13051  grpinvid1  13124  grpinvid2  13125  mulgp1  13225  ghmlin  13318  ghmsub  13321  cmncom  13372  islss3  13875  unopn  14173  innei  14331  cncfi  14733