Theorem 3impb 1201

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

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

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 982

This theorem is referenced by:  3adant1l  1232  3adant1r  1233  3impdi  1305  vtocl3gf  2835  rspc2ev  2891  reuss  3453  trssord  4425  funtp  5321  resdif  5538  funimass4  5623  fnovex  5967  fnotovb  5978  fovcdm  6079  fnovrn  6084  fmpoco  6292  nndi  6562  nnaordi  6584  ecovass  6721  ecoviass  6722  ecovdi  6723  ecovidi  6724  eqsupti  7080  addasspig  7425  mulasspig  7427  distrpig  7428  distrnq0  7554  addassnq0  7557  distnq0r  7558  prcdnql  7579  prcunqu  7580  genpassl  7619  genpassu  7620  genpassg  7621  distrlem1prl  7677  distrlem1pru  7678  ltexprlemopl  7696  ltexprlemopu  7698  le2tri3i  8163  cnegexlem1  8229  subadd  8257  addsub  8265  subdi  8439  submul2  8453  div12ap  8749  diveqap1  8760  divnegap  8761  divdivap2  8779  ltmulgt11  8919  gt0div  8925  ge0div  8926  uzind3  9468  fnn0ind  9471  qdivcl  9746  irrmul  9750  xrlttr  9899  fzen  10147  ccatval21sw  11036  lswccatn0lsw  11042  lenegsq  11325  moddvds  12029  dvds2add  12055  dvds2sub  12056  dvdsleabs  12075  divalgb  12155  ndvdsadd  12161  modgcd  12231  absmulgcd  12257  odzval  12483  pcmul  12543  setsresg  12789  prdssgrpd  13165  issubmnd  13192  prdsmndd  13198  submcl  13229  grpinvid1  13302  grpinvid2  13303  mulgp1  13409  ghmlin  13502  ghmsub  13505  cmncom  13556  islss3  14059  unopn  14395  innei  14553  cncfi  14968