Theorem 3impb 1226

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

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

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 1007

This theorem is referenced by:  3adant1l  1257  3adant1r  1258  3impdi  1330  vtocl3gf  2878  rspc2ev  2936  reuss  3502  trssord  4501  funtp  5409  resdif  5636  funimass4  5727  fnovex  6083  fnotovb  6096  fovcdm  6197  fnovrn  6202  fmpoco  6412  nndi  6719  nnaordi  6741  ecovass  6878  ecoviass  6879  ecovdi  6880  ecovidi  6881  eqsupti  7287  addasspig  7645  mulasspig  7647  distrpig  7648  distrnq0  7774  addassnq0  7777  distnq0r  7778  prcdnql  7799  prcunqu  7800  genpassl  7839  genpassu  7840  genpassg  7841  distrlem1prl  7897  distrlem1pru  7898  ltexprlemopl  7916  ltexprlemopu  7918  le2tri3i  8382  cnegexlem1  8448  subadd  8476  addsub  8484  subdi  8658  submul2  8672  div12ap  8968  diveqap1  8979  divnegap  8980  divdivap2  8998  ltmulgt11  9138  gt0div  9144  ge0div  9145  uzind3  9691  fnn0ind  9694  qdivcl  9975  irrmul  9979  xrlttr  10128  fzen  10377  ccatval21sw  11293  lswccatn0lsw  11299  swrdwrdsymbg  11356  ccatpfx  11393  ccatopth  11408  lenegsq  11780  moddvds  12485  dvds2add  12511  dvds2sub  12512  dvdsleabs  12531  divalgb  12611  ndvdsadd  12617  modgcd  12687  absmulgcd  12713  odzval  12939  pcmul  12999  setsresg  13250  prdssgrpd  13628  issubmnd  13655  prdsmndd  13661  submcl  13692  grpinvid1  13765  grpinvid2  13766  mulgp1  13872  ghmlin  13965  ghmsub  13968  cmncom  14019  islss3  14527  unopn  14870  innei  15028  cncfi  15443