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  4471  funtp  5374  resdif  5596  funimass4  5686  fnovex  6040  fnotovb  6053  fovcdm  6154  fnovrn  6159  fmpoco  6368  nndi  6640  nnaordi  6662  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  eqsupti  7174  addasspig  7528  mulasspig  7530  distrpig  7531  distrnq0  7657  addassnq0  7660  distnq0r  7661  prcdnql  7682  prcunqu  7683  genpassl  7722  genpassu  7723  genpassg  7724  distrlem1prl  7780  distrlem1pru  7781  ltexprlemopl  7799  ltexprlemopu  7801  le2tri3i  8266  cnegexlem1  8332  subadd  8360  addsub  8368  subdi  8542  submul2  8556  div12ap  8852  diveqap1  8863  divnegap  8864  divdivap2  8882  ltmulgt11  9022  gt0div  9028  ge0div  9029  uzind3  9571  fnn0ind  9574  qdivcl  9850  irrmul  9854  xrlttr  10003  fzen  10251  ccatval21sw  11153  lswccatn0lsw  11159  swrdwrdsymbg  11211  ccatpfx  11248  ccatopth  11263  lenegsq  11621  moddvds  12325  dvds2add  12351  dvds2sub  12352  dvdsleabs  12371  divalgb  12451  ndvdsadd  12457  modgcd  12527  absmulgcd  12553  odzval  12779  pcmul  12839  setsresg  13085  prdssgrpd  13463  issubmnd  13490  prdsmndd  13496  submcl  13527  grpinvid1  13600  grpinvid2  13601  mulgp1  13707  ghmlin  13800  ghmsub  13803  cmncom  13854  islss3  14358  unopn  14694  innei  14852  cncfi  15267