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  5527  funimass4  5612  fnovex  5956  fnotovb  5967  fovcdm  6068  fnovrn  6073  fmpoco  6276  nndi  6546  nnaordi  6568  ecovass  6705  ecoviass  6706  ecovdi  6707  ecovidi  6708  eqsupti  7064  addasspig  7400  mulasspig  7402  distrpig  7403  distrnq0  7529  addassnq0  7532  distnq0r  7533  prcdnql  7554  prcunqu  7555  genpassl  7594  genpassu  7595  genpassg  7596  distrlem1prl  7652  distrlem1pru  7653  ltexprlemopl  7671  ltexprlemopu  7673  le2tri3i  8138  cnegexlem1  8204  subadd  8232  addsub  8240  subdi  8414  submul2  8428  div12ap  8724  diveqap1  8735  divnegap  8736  divdivap2  8754  ltmulgt11  8894  gt0div  8900  ge0div  8901  uzind3  9442  fnn0ind  9445  qdivcl  9720  irrmul  9724  xrlttr  9873  fzen  10121  lenegsq  11263  moddvds  11967  dvds2add  11993  dvds2sub  11994  dvdsleabs  12013  divalgb  12093  ndvdsadd  12099  modgcd  12169  absmulgcd  12195  odzval  12421  pcmul  12481  setsresg  12727  issubmnd  13109  submcl  13137  grpinvid1  13210  grpinvid2  13211  mulgp1  13311  ghmlin  13404  ghmsub  13407  cmncom  13458  islss3  13961  unopn  14267  innei  14425  cncfi  14840