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  2864  rspc2ev  2922  reuss  3485  trssord  4470  funtp  5373  resdif  5593  funimass4  5683  fnovex  6033  fnotovb  6046  fovcdm  6147  fnovrn  6152  fmpoco  6360  nndi  6630  nnaordi  6652  ecovass  6789  ecoviass  6790  ecovdi  6791  ecovidi  6792  eqsupti  7159  addasspig  7513  mulasspig  7515  distrpig  7516  distrnq0  7642  addassnq0  7645  distnq0r  7646  prcdnql  7667  prcunqu  7668  genpassl  7707  genpassu  7708  genpassg  7709  distrlem1prl  7765  distrlem1pru  7766  ltexprlemopl  7784  ltexprlemopu  7786  le2tri3i  8251  cnegexlem1  8317  subadd  8345  addsub  8353  subdi  8527  submul2  8541  div12ap  8837  diveqap1  8848  divnegap  8849  divdivap2  8867  ltmulgt11  9007  gt0div  9013  ge0div  9014  uzind3  9556  fnn0ind  9559  qdivcl  9834  irrmul  9838  xrlttr  9987  fzen  10235  ccatval21sw  11135  lswccatn0lsw  11141  swrdwrdsymbg  11191  ccatpfx  11228  ccatopth  11243  lenegsq  11601  moddvds  12305  dvds2add  12331  dvds2sub  12332  dvdsleabs  12351  divalgb  12431  ndvdsadd  12437  modgcd  12507  absmulgcd  12533  odzval  12759  pcmul  12819  setsresg  13065  prdssgrpd  13443  issubmnd  13470  prdsmndd  13476  submcl  13507  grpinvid1  13580  grpinvid2  13581  mulgp1  13687  ghmlin  13780  ghmsub  13783  cmncom  13834  islss3  14337  unopn  14673  innei  14831  cncfi  15246