Theorem 3impb 1225

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

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

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 1006

This theorem is referenced by:  3adant1l  1256  3adant1r  1257  3impdi  1329  vtocl3gf  2867  rspc2ev  2925  reuss  3488  trssord  4477  funtp  5383  resdif  5605  funimass4  5696  fnovex  6051  fnotovb  6064  fovcdm  6165  fnovrn  6170  fmpoco  6381  nndi  6654  nnaordi  6676  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  eqsupti  7195  addasspig  7550  mulasspig  7552  distrpig  7553  distrnq0  7679  addassnq0  7682  distnq0r  7683  prcdnql  7704  prcunqu  7705  genpassl  7744  genpassu  7745  genpassg  7746  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  le2tri3i  8288  cnegexlem1  8354  subadd  8382  addsub  8390  subdi  8564  submul2  8578  div12ap  8874  diveqap1  8885  divnegap  8886  divdivap2  8904  ltmulgt11  9044  gt0div  9050  ge0div  9051  uzind3  9593  fnn0ind  9596  qdivcl  9877  irrmul  9881  xrlttr  10030  fzen  10278  ccatval21sw  11186  lswccatn0lsw  11192  swrdwrdsymbg  11249  ccatpfx  11286  ccatopth  11301  lenegsq  11660  moddvds  12365  dvds2add  12391  dvds2sub  12392  dvdsleabs  12411  divalgb  12491  ndvdsadd  12497  modgcd  12567  absmulgcd  12593  odzval  12819  pcmul  12879  setsresg  13125  prdssgrpd  13503  issubmnd  13530  prdsmndd  13536  submcl  13567  grpinvid1  13640  grpinvid2  13641  mulgp1  13747  ghmlin  13840  ghmsub  13843  cmncom  13894  islss3  14399  unopn  14735  innei  14893  cncfi  15308