Theorem 3impb 1223

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

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

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 1004

This theorem is referenced by:  3adant1l  1254  3adant1r  1255  3impdi  1327  vtocl3gf  2865  rspc2ev  2923  reuss  3486  trssord  4475  funtp  5380  resdif  5602  funimass4  5692  fnovex  6046  fnotovb  6059  fovcdm  6160  fnovrn  6165  fmpoco  6376  nndi  6649  nnaordi  6671  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  eqsupti  7186  addasspig  7540  mulasspig  7542  distrpig  7543  distrnq0  7669  addassnq0  7672  distnq0r  7673  prcdnql  7694  prcunqu  7695  genpassl  7734  genpassu  7735  genpassg  7736  distrlem1prl  7792  distrlem1pru  7793  ltexprlemopl  7811  ltexprlemopu  7813  le2tri3i  8278  cnegexlem1  8344  subadd  8372  addsub  8380  subdi  8554  submul2  8568  div12ap  8864  diveqap1  8875  divnegap  8876  divdivap2  8894  ltmulgt11  9034  gt0div  9040  ge0div  9041  uzind3  9583  fnn0ind  9586  qdivcl  9867  irrmul  9871  xrlttr  10020  fzen  10268  ccatval21sw  11172  lswccatn0lsw  11178  swrdwrdsymbg  11235  ccatpfx  11272  ccatopth  11287  lenegsq  11646  moddvds  12350  dvds2add  12376  dvds2sub  12377  dvdsleabs  12396  divalgb  12476  ndvdsadd  12482  modgcd  12552  absmulgcd  12578  odzval  12804  pcmul  12864  setsresg  13110  prdssgrpd  13488  issubmnd  13515  prdsmndd  13521  submcl  13552  grpinvid1  13625  grpinvid2  13626  mulgp1  13732  ghmlin  13825  ghmsub  13828  cmncom  13879  islss3  14383  unopn  14719  innei  14877  cncfi  15292