Theorem 3adant3 961

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 938	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

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

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 924

This theorem is referenced by:  stoic4a  1364  stoic4b  1365  vtoclgft  2663  eqeu  2776  tpssi  3586  issod  4119  sotricim  4123  soinxp  4475  funopg  5010  fnco  5084  resasplitss  5147  resdif  5232  fnimapr  5321  ftpg  5438  fsnunfv  5454  fvpr1g  5458  fvpr2g  5459  f1ocnvfvb  5514  f1oiso2  5561  moriotass  5591  f1ofveu  5595  acexmid  5606  ovig  5717  ov6g  5733  ovg  5734  ot1stg  5874  ot2ndg  5875  poxp  5948  brtposg  5967  smores3  6006  smoiso  6015  rdgivallem  6094  frecsuclem  6119  nnaord  6214  nnaword  6216  nnawordex  6233  ecopovtrn  6335  ecopovtrng  6338  xpdom3m  6496  mapxpen  6510  sbthlemi4  6606  ltsopi  6816  addcanpig  6830  distrnqg  6883  ltsonq  6894  ltanqg  6896  ltmnqg  6897  nnanq0  6954  distrnq0  6955  distnq0r  6959  prarloclem  6997  genpassl  7020  genpassu  7021  distrlem1prl  7078  distrlem1pru  7079  distrlem5prl  7082  distrlem5pru  7083  1idprl  7086  1idpru  7087  ltpopr  7091  ltsopr  7092  ltexprlemm  7096  ltexprlemfl  7105  ltexprlemfu  7107  addcanprlemu  7111  recexprlem1ssl  7129  recexprlem1ssu  7130  aptipr  7137  lttrsr  7245  ltsosr  7247  ltasrg  7253  recexgt0sr  7256  mulextsr1  7263  axmulass  7345  ltxrlt  7489  axltwlin  7491  axlttrn  7492  axltadd  7493  letr  7505  mul12  7548  add12  7577  subadd  7622  addsub  7630  npncan  7640  nppcan  7641  nnpcan  7642  nppcan3  7643  pnpcan  7658  pnncan  7660  ppncan  7661  subdi  7800  ltaddsub2  7852  leaddsub2  7854  ltaddsublt  7982  apreap  7998  lemul1  8004  reapmul1lem  8005  reapadd1  8007  reapcotr  8009  receuap  8070  divassap  8089  div23ap  8090  divmulassap  8094  divmulasscomap  8095  divcanap4  8098  divsubdirap  8107  divcanap5  8113  divdiv32ap  8119  divdivap2  8123  letrp1  8237  ltmulgt12  8254  lediv1  8258  ltdiv2  8276  lediv2  8280  lbinfle  8339  xrletr  9198  xrre2  9208  ixxdisj  9246  ubioc1  9272  lbico1  9273  elioo5  9276  iccsupr  9309  lbicc2  9326  ubicc2  9327  iccneg  9331  icoshft  9332  icodisj  9334  iccf1o  9346  zltaddlt1le  9348  fztri3or  9378  fzdcel  9379  fzen  9382  uzsubsubfz  9386  fzrevral2  9443  fzshftral  9445  fz0fzdiffz0  9462  difelfznle  9467  fzo1fzo0n0  9515  fzonmapblen  9519  fzosubel2  9527  ubmelfzo  9532  elfzodifsumelfzo  9533  ssfzo12bi  9557  ubmelm1fzo  9558  subfzo0  9574  ceiqle  9641  modqid2  9679  zmodidfzoimp  9682  addmodidr  9701  modfzo0difsn  9723  addmodlteq  9726  frec2uzf1od  9734  exprecap  9887  expdivap  9897  expubnd  9903  sqdivap  9910  mulbinom2  9959  bernneq2  9964  bcval3  10048  bccmpl  10051  omgadd  10099  shftval2  10149  mulreap  10186  elicc4abs  10415  abssubge0  10423  abssuble0  10424  maxleast  10534  maxltsup  10539  dvdscmul  10690  summodnegmod  10694  modmulconst  10695  dvdsleabs  10713  dvdsleabs2  10714  addmodlteqALT  10727  dvdsexp  10729  mulmoddvds  10731  divalgb  10792  divgcdz  10830  gcdass  10871  mulgcdr  10874  gcddiv  10875  lcmass  10934  coprmdvds  10941  qredeq  10945  qredeu  10946  congr  10949  divgcdcoprm0  10950  divgcdcoprmex  10951  cncongr1  10952  cncongr2  10953  isprm3  10967  dvdsnprmd  10974  euclemma  10992  prmdvdsexpb  10995  prmexpb  10997  rpexp  10999  znege1  11023