Theorem 3adant3 958

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 935	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  stoic4a  1361  stoic4b  1362  vtoclgft  2649  eqeu  2762  tpssi  3551  issod  4074  sotricim  4078  soinxp  4428  funopg  4954  fnco  5027  resasplitss  5089  resdif  5168  fnimapr  5254  ftpg  5368  fsnunfv  5384  fvpr1g  5388  fvpr2g  5389  f1ocnvfvb  5440  f1oiso2  5486  moriotass  5516  f1ofveu  5520  acexmid  5531  ovig  5642  ov6g  5658  ovg  5659  ot1stg  5799  ot2ndg  5800  poxp  5873  brtposg  5892  smores3  5931  smoiso  5940  rdgivallem  5991  frecsuclemdm  6011  frecsuclem3  6013  nnaord  6105  nnaword  6107  nnawordex  6124  ecopovtrn  6226  ecopovtrng  6229  xpdom3m  6331  ltsopi  6510  addcanpig  6524  distrnqg  6577  ltsonq  6588  ltanqg  6590  ltmnqg  6591  nnanq0  6648  distrnq0  6649  distnq0r  6653  prarloclem  6691  genpassl  6714  genpassu  6715  distrlem1prl  6772  distrlem1pru  6773  distrlem5prl  6776  distrlem5pru  6777  1idprl  6780  1idpru  6781  ltpopr  6785  ltsopr  6786  ltexprlemm  6790  ltexprlemfl  6799  ltexprlemfu  6801  addcanprlemu  6805  recexprlem1ssl  6823  recexprlem1ssu  6824  aptipr  6831  lttrsr  6939  ltsosr  6941  ltasrg  6947  recexgt0sr  6950  mulextsr1  6957  axmulass  7039  ltxrlt  7178  axltwlin  7180  axlttrn  7181  axltadd  7182  letr  7194  mul12  7237  add12  7266  subadd  7311  addsub  7319  npncan  7329  nppcan  7330  nnpcan  7331  nppcan3  7332  pnpcan  7347  pnncan  7349  ppncan  7350  subdi  7489  ltaddsub2  7541  leaddsub2  7543  ltaddsublt  7671  apreap  7687  lemul1  7693  reapmul1lem  7694  reapadd1  7696  reapcotr  7698  receuap  7759  divassap  7778  div23ap  7779  divmulassap  7783  divmulasscomap  7784  divcanap4  7787  divsubdirap  7796  divcanap5  7802  divdiv32ap  7808  divdivap2  7812  letrp1  7926  ltmulgt12  7943  lediv1  7947  ltdiv2  7965  lediv2  7969  lbinfle  8028  xrletr  8878  xrre2  8888  ixxdisj  8926  ubioc1  8952  lbico1  8953  elioo5  8956  iccsupr  8989  lbicc2  9006  ubicc2  9007  iccneg  9011  icoshft  9012  icodisj  9014  iccf1o  9026  zltaddlt1le  9028  fztri3or  9058  fzdcel  9059  fzen  9062  uzsubsubfz  9066  fzrevral2  9123  fzshftral  9125  fz0fzdiffz0  9141  difelfznle  9146  fzo1fzo0n0  9192  fzonmapblen  9196  fzosubel2  9204  ubmelfzo  9209  elfzodifsumelfzo  9210  ssfzo12bi  9234  ubmelm1fzo  9235  subfzo0  9251  ceiqle  9315  modqid2  9353  zmodidfzoimp  9356  addmodidr  9375  modfzo0difsn  9397  addmodlteq  9400  frec2uzf1od  9408  exprecap  9517  expdivap  9527  expubnd  9533  sqdivap  9540  mulbinom2  9589  bernneq2  9594  bcval3  9678  bccmpl  9681  shftval2  9714  mulreap  9751  elicc4abs  9980  abssubge0  9988  abssuble0  9989  maxleast  10099  maxltsup  10104  dvdscmul  10222  summodnegmod  10226  modmulconst  10227  dvdsleabs  10245  dvdsleabs2  10246  addmodlteqALT  10259  dvdsexp  10261  mulmoddvds  10263  divalgb  10325  divgcdz  10363  gcdass  10404  mulgcdr  10407  gcddiv  10408  lcmass  10467  coprmdvds  10474  qredeq  10478  qredeu  10479  congr  10482  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm3  10500  dvdsnprmd  10507  euclemma  10525  prmdvdsexpb  10528  prmexpb  10530  rpexp  10532  znege1  10556