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  8435  cnegexlem1  8502  subadd  8530  addsub  8538  subdi  8713  submul2  8727  div12ap  9026  diveqap1  9037  divnegap  9038  divdivap2  9056  ltmulgt11  9196  gt0div  9202  ge0div  9203  uzind3  9763  fnn0ind  9766  qdivcl  10052  irrmul  10057  xrlttr  10207  fzen  10457  ccatval21sw  11387  lswccatn0lsw  11393  swrdwrdsymbg  11450  ccatpfx  11487  ccatopth  11502  lenegsq  11876  moddvds  12582  dvds2add  12608  dvds2sub  12609  dvdsleabs  12628  divalgb  12708  ndvdsadd  12714  modgcd  12784  absmulgcd  12810  odzval  13040  pcmul  13100  setsresg  13439  issubmnd  13804  submcl  13835  grpinvid1  13906  grpinvid2  13907  mulgp1  14007  ghmlin  14100  ghmsub  14103  cmncom  14154  prdssgrpd  14240  prdsmndd  14243  islss3  14765  unopn  15155  innei  15313  cncfi  15728