Theorem 3impb 1202

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

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

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 983

This theorem is referenced by:  3adant1l  1233  3adant1r  1234  3impdi  1306  vtocl3gf  2838  rspc2ev  2896  reuss  3458  trssord  4435  funtp  5336  resdif  5556  funimass4  5642  fnovex  5990  fnotovb  6001  fovcdm  6102  fnovrn  6107  fmpoco  6315  nndi  6585  nnaordi  6607  ecovass  6744  ecoviass  6745  ecovdi  6746  ecovidi  6747  eqsupti  7113  addasspig  7463  mulasspig  7465  distrpig  7466  distrnq0  7592  addassnq0  7595  distnq0r  7596  prcdnql  7617  prcunqu  7618  genpassl  7657  genpassu  7658  genpassg  7659  distrlem1prl  7715  distrlem1pru  7716  ltexprlemopl  7734  ltexprlemopu  7736  le2tri3i  8201  cnegexlem1  8267  subadd  8295  addsub  8303  subdi  8477  submul2  8491  div12ap  8787  diveqap1  8798  divnegap  8799  divdivap2  8817  ltmulgt11  8957  gt0div  8963  ge0div  8964  uzind3  9506  fnn0ind  9509  qdivcl  9784  irrmul  9788  xrlttr  9937  fzen  10185  ccatval21sw  11084  lswccatn0lsw  11090  swrdwrdsymbg  11140  ccatpfx  11177  ccatopth  11192  lenegsq  11481  moddvds  12185  dvds2add  12211  dvds2sub  12212  dvdsleabs  12231  divalgb  12311  ndvdsadd  12317  modgcd  12387  absmulgcd  12413  odzval  12639  pcmul  12699  setsresg  12945  prdssgrpd  13322  issubmnd  13349  prdsmndd  13355  submcl  13386  grpinvid1  13459  grpinvid2  13460  mulgp1  13566  ghmlin  13659  ghmsub  13662  cmncom  13713  islss3  14216  unopn  14552  innei  14710  cncfi  15125