Theorem 3adant3 1041

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

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

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  stoic4a  1474  stoic4b  1475  vtoclgft  2851  eqeu  2973  ssprsseq  3829  tpssi  3836  issod  4409  sotricim  4413  soinxp  4788  funopg  5351  fnco  5430  resasplitss  5504  resdif  5593  fnimapr  5693  ftpg  5822  fsnunfv  5839  fvpr1g  5844  fvpr2g  5845  f1ocnvfvb  5903  f1oiso2  5950  moriotass  5984  f1ofveu  5988  acexmid  5999  ovig  6125  ov6g  6142  ovg  6143  ot1stg  6296  ot2ndg  6297  poxp  6376  brtposg  6398  smores3  6437  smoiso  6446  rdgivallem  6525  frecsuclem  6550  nnaord  6653  nnaword  6655  nnawordex  6673  ecopovtrn  6777  ecopovtrng  6780  xpdom3m  6989  mapxpen  7005  sbthlemi4  7123  djuenun  7390  netap  7436  2omotaplemap  7439  ltsopi  7503  addcanpig  7517  distrnqg  7570  ltsonq  7581  ltanqg  7583  ltmnqg  7584  nnanq0  7641  distrnq0  7642  distnq0r  7646  prarloclem  7684  genpassl  7707  genpassu  7708  distrlem1prl  7765  distrlem1pru  7766  distrlem5prl  7769  distrlem5pru  7770  1idprl  7773  1idpru  7774  ltpopr  7778  ltsopr  7779  ltexprlemm  7783  ltexprlemfl  7792  ltexprlemfu  7794  addcanprlemu  7798  recexprlem1ssl  7816  recexprlem1ssu  7817  aptipr  7824  lttrsr  7945  ltsosr  7947  ltasrg  7953  recexgt0sr  7956  mulextsr1  7964  axmulass  8056  ltxrlt  8208  axltwlin  8210  axlttrn  8211  axltadd  8212  letr  8225  mul12  8271  add12  8300  subadd  8345  addsub  8353  npncan  8363  nppcan  8364  nnpcan  8365  nppcan3  8366  pnpcan  8381  pnncan  8383  ppncan  8384  subdi  8527  ltaddsub2  8580  leaddsub2  8582  ltaddsublt  8714  apreap  8730  lemul1  8736  reapmul1lem  8737  reapadd1  8739  reapcotr  8741  receuap  8812  divassap  8833  div23ap  8834  divmulassap  8838  divmulasscomap  8839  divcanap4  8842  divsubdirap  8851  divcanap5  8857  divdiv32ap  8863  divdivap2  8867  div2subap  8980  letrp1  8991  ltmulgt12  9008  lediv1  9012  ltdiv2  9030  lediv2  9034  lbinfle  9093  difgtsumgt  9512  xrletr  10000  xrre2  10013  xaddass  10061  ixxdisj  10095  ubioc1  10121  lbico1  10122  elioo5  10125  iccsupr  10158  lbicc2  10176  ubicc2  10177  iccneg  10181  icoshft  10182  icodisj  10184  iccf1o  10196  iccen  10198  zltaddlt1le  10199  fztri3or  10231  fzdcel  10232  fzen  10235  uzsubsubfz  10239  fzrevral2  10298  fzshftral  10300  fz0fzdiffz0  10322  difelfznle  10327  fzo1fzo0n0  10379  fzonmapblen  10383  fzosubel2  10396  ubmelfzo  10401  elfzodifsumelfzo  10402  ssfzo12bi  10426  ubmelm1fzo  10427  subfzo0  10443  ceiqle  10530  modqid2  10568  zmodidfzoimp  10571  addmodidr  10590  modfzo0difsn  10612  addmodlteq  10615  frec2uzf1od  10623  exprecap  10797  expdivap  10807  expubnd  10813  sqdivap  10820  mulbinom2  10873  bernneq2  10878  mulsubdivbinom2ap  10928  bcval3  10968  bccmpl  10971  omgadd  11019  ccatval1  11127  ccatval2  11128  ccatass  11138  lswccatn0lsw  11141  ccatws1lenp1bg  11163  pfxfv  11211  pfxnd  11216  pfxtrcfv  11220  pfxsuffeqwrdeq  11225  swrdswrd  11232  pfxpfx  11235  ccatopth2  11244  pfxccatin12lem4  11253  pfxccatin12lem1  11255  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  pfxccatpfx1  11263  pfxccatpfx2  11264  s3fv0g  11318  s3fv1g  11319  shftval2  11332  mulreap  11370  elicc4abs  11600  abssubge0  11608  abssuble0  11609  maxleast  11719  maxltsup  11724  xrmaxltsup  11764  xrmineqinf  11775  xrltmininf  11776  xrlemininf  11777  fsumdifsnconst  11961  prodfap0  12051  prodfrecap  12052  fprodabs  12122  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  dvdscmul  12324  summodnegmod  12328  modmulconst  12329  dvdsleabs  12351  dvdsleabs2  12352  addmodlteqALT  12365  dvdsexp  12367  mulmoddvds  12369  divalgb  12431  divgcdz  12487  gcdass  12531  mulgcdr  12534  gcddiv  12535  uzwodc  12553  lcmass  12602  coprmdvds  12609  qredeq  12613  qredeu  12614  congr  12617  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  isprm3  12635  dvdsnprmd  12642  euclemma  12663  prmdvdsexpb  12666  prmexpb  12668  rpexp  12670  znege1  12695  modprminv  12767  modprminveq  12768  vfermltl  12769  modprm0  12772  modprmn0modprm0  12774  coprimeprodsq  12775  coprimeprodsq2  12776  pythagtriplem1  12783  pythagtriplem3  12785  pythagtriplem6  12788  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem14  12795  pythagtriplem16  12797  pythagtriplem19  12800  pythagtrip  12801  pcmul  12819  pcdiv  12820  pcqcl  12824  pcgcd1  12846  pcgcd  12847  dvdsprmpweq  12853  difsqpwdvds  12856  pcfaclem  12867  unbendc  13020  strle3g  13136  ercpbl  13359  grpinvid1  13580  grpinvid2  13581  grpasscan1  13591  grpasscan2  13592  grpidrcan  13593  grpidlcan  13594  grpinvadd  13606  grpsubadd  13616  grppncan  13619  pwsinvg  13640  qussub  13769  subcmnd  13865  mulgass2  14016  dvrcan1  14098  dvrcan3  14099  rmodislmodlem  14308  rmodislmod  14309  islssm  14315  lsselg  14319  lspss  14357  lspssp  14361  lsslsp  14387  islidlm  14437  lidlnegcl  14443  lidlsubcl  14445  zndvds  14607  basgen  14748  clsss  14786  ntrin  14792  ntrcls0  14799  neiint  14813  neiss  14818  neipsm  14822  opnssneib  14824  innei  14831  restco  14842  iscnp  14867  cnconst2  14901  txcn  14943  psmetsym  14997  psmetlecl  15002  distspace  15003  xmetlecl  15035  xmetsym  15036  xblcntrps  15081  xblcntr  15082  blssec  15106  blpnfctr  15107  txmetcn  15187  cnmet  15198  dvid  15363  dvidre  15365  dvply1  15433  ptolemy  15492  sinq12gt0  15498  sincosq1eq  15507  rpcxpsub  15576  relogbexpap  15626  logbleb  15629  logblt  15630  rplogbcxp  15631  lgsval4  15693  lgsmod  15699  lgsne0  15711  lgsmulsqcoprm  15719  2lgsoddprmlem1  15778  structiedg0val  15835  lpvtx  15873  upgredg2vtx  15940  upgredgpr  15941  ushgredgedg  16018  ushgredgedgloop  16020