Theorem 3impb 1230

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3adant1l  1261  3adant1r  1262  3impdi  1334  vtocl3gf  2886  rspc2ev  2945  reuss  3514  trssord  4525  funtp  5434  resdif  5661  funimass4  5753  fnovex  6118  fnotovb  6131  fovcdm  6232  fnovrn  6237  fmpoco  6452  nndi  6759  nnaordi  6781  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  eqsupti  7336  addasspig  7697  mulasspig  7699  distrpig  7700  distrnq0  7826  addassnq0  7829  distnq0r  7830  prcdnql  7851  prcunqu  7852  genpassl  7891  genpassu  7892  genpassg  7893  distrlem1prl  7949  distrlem1pru  7950  ltexprlemopl  7968  ltexprlemopu  7970  le2tri3i  8434  cnegexlem1  8501  subadd  8529  addsub  8537  subdi  8712  submul2  8726  div12ap  9024  diveqap1  9035  divnegap  9036  divdivap2  9054  ltmulgt11  9194  gt0div  9200  ge0div  9201  uzind3  9759  fnn0ind  9762  qdivcl  10043  irrmul  10047  xrlttr  10197  fzen  10447  ccatval21sw  11373  lswccatn0lsw  11379  swrdwrdsymbg  11436  ccatpfx  11473  ccatopth  11488  lenegsq  11861  moddvds  12566  dvds2add  12592  dvds2sub  12593  dvdsleabs  12612  divalgb  12692  ndvdsadd  12698  modgcd  12768  absmulgcd  12794  odzval  13020  pcmul  13080  setsresg  13390  issubmnd  13755  submcl  13786  grpinvid1  13857  grpinvid2  13858  mulgp1  13958  ghmlin  14051  ghmsub  14054  cmncom  14105  prdssgrpd  14191  prdsmndd  14194  islss3  14716  unopn  15106  innei  15264  cncfi  15679