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  2880  rspc2ev  2939  reuss  3506  trssord  4506  funtp  5414  resdif  5641  funimass4  5732  fnovex  6091  fnotovb  6104  fovcdm  6205  fnovrn  6210  fmpoco  6425  nndi  6732  nnaordi  6754  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  eqsupti  7300  addasspig  7661  mulasspig  7663  distrpig  7664  distrnq0  7790  addassnq0  7793  distnq0r  7794  prcdnql  7815  prcunqu  7816  genpassl  7855  genpassu  7856  genpassg  7857  distrlem1prl  7913  distrlem1pru  7914  ltexprlemopl  7932  ltexprlemopu  7934  le2tri3i  8398  cnegexlem1  8464  subadd  8492  addsub  8500  subdi  8675  submul2  8689  div12ap  8985  diveqap1  8996  divnegap  8997  divdivap2  9015  ltmulgt11  9155  gt0div  9161  ge0div  9162  uzind3  9709  fnn0ind  9712  qdivcl  9993  irrmul  9997  xrlttr  10147  fzen  10397  ccatval21sw  11318  lswccatn0lsw  11324  swrdwrdsymbg  11381  ccatpfx  11418  ccatopth  11433  lenegsq  11805  moddvds  12510  dvds2add  12536  dvds2sub  12537  dvdsleabs  12556  divalgb  12636  ndvdsadd  12642  modgcd  12712  absmulgcd  12738  odzval  12964  pcmul  13024  setsresg  13334  issubmnd  13703  submcl  13734  grpinvid1  13807  grpinvid2  13808  mulgp1  13908  ghmlin  14001  ghmsub  14004  cmncom  14055  prdssgrpd  14133  prdsmndd  14136  islss3  14653  unopn  14996  innei  15154  cncfi  15569