Theorem 3adant3 1048

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  stoic4a  1481  stoic4b  1482  vtoclgft  2873  eqeu  2996  ssprsseq  3877  tpssi  3884  issod  4464  sotricim  4468  soinxp  4845  funopg  5411  fnco  5491  resasplitss  5569  resdif  5661  fnimapr  5763  ftpg  5899  fsnunfv  5916  fvpr1g  5921  fvpr2g  5922  f1ocnvfvb  5986  f1oiso2  6033  moriotass  6069  f1ofveu  6073  acexmid  6084  ovig  6210  ov6g  6227  ovg  6228  ot1stg  6386  ot2ndg  6387  poxp  6468  suppvalfn  6481  suppsnopdc  6490  suppfnss  6497  funsssuppss  6498  brtposg  6525  smores3  6564  smoiso  6573  rdgivallem  6652  frecsuclem  6677  nnaord  6782  nnaword  6784  nnawordex  6802  ecopovtrn  6906  ecopovtrng  6909  xpdom3m  7132  mapxpen  7148  sbthlemi4  7277  djuenun  7569  netap  7621  2omotaplemap  7624  ltsopi  7688  addcanpig  7702  distrnqg  7755  ltsonq  7766  ltanqg  7768  ltmnqg  7769  nnanq0  7826  distrnq0  7827  distnq0r  7831  prarloclem  7869  genpassl  7892  genpassu  7893  distrlem1prl  7950  distrlem1pru  7951  distrlem5prl  7954  distrlem5pru  7955  1idprl  7958  1idpru  7959  ltpopr  7963  ltsopr  7964  ltexprlemm  7968  ltexprlemfl  7977  ltexprlemfu  7979  addcanprlemu  7983  recexprlem1ssl  8001  recexprlem1ssu  8002  aptipr  8009  lttrsr  8130  ltsosr  8132  ltasrg  8138  recexgt0sr  8141  mulextsr1  8149  axmulass  8241  ltxrlt  8392  axltwlin  8394  axlttrn  8395  axltadd  8396  letr  8409  mul12  8457  add12  8486  subadd  8531  addsub  8539  npncan  8549  nppcan  8550  nnpcan  8551  nppcan3  8552  pnpcan  8567  pnncan  8569  ppncan  8570  subdi  8714  ltaddsub2  8767  leaddsub2  8769  ltaddsublt  8902  apreap  8918  lemul1  8924  reapmul1lem  8925  reapadd1  8927  reapcotr  8929  receuap  9002  divassap  9023  div23ap  9024  divmulassap  9028  divmulasscomap  9029  divcanap4  9032  divsubdirap  9041  divcanap5  9047  divdiv32ap  9053  divdivap2  9057  div2subap  9170  letrp1  9181  ltmulgt12  9198  lediv1  9202  ltdiv2  9220  lediv2  9224  lbinfle  9283  indfdc  9301  indfval  9302  difgtsumgt  9719  xrletr  10221  xrre2  10234  xaddass  10282  ixxdisj  10316  ubioc1  10342  lbico1  10343  elioo5  10346  iccsupr  10379  lbicc2  10397  ubicc2  10398  iccneg  10402  icoshft  10403  icodisj  10405  lincmble  10417  iccf1o  10418  iccen  10420  zltaddlt1le  10421  fztri3or  10454  fzdcel  10455  fzen  10458  uzsubsubfz  10463  fzrevral2  10524  fzshftral  10526  fz0fzdiffz0  10548  difelfznle  10553  fzo1fzo0n0  10606  fzonmapblen  10610  fzosubel2  10624  ubmelfzo  10629  elfzodifsumelfzo  10630  ssfzo12bi  10654  ubmelm1fzo  10655  subfzo0  10672  ceiqle  10765  modqid2  10803  zmodidfzoimp  10806  addmodidr  10825  modfzo0difsn  10847  addmodlteq  10850  frec2uzf1od  10858  exprecap  11032  expdivap  11042  expubnd  11048  sqdivap  11055  mulbinom2  11108  bernneq2  11114  mulsubdivbinom2ap  11165  bcval3  11205  bccmpl  11208  omgadd  11258  ccatval1  11381  ccatval2  11382  ccatass  11392  lswccatn0lsw  11395  ccatws1lenp1bg  11419  ccatw2s1leng  11422  pfxfv  11472  pfxnd  11477  pfxtrcfv  11481  pfxsuffeqwrdeq  11486  swrdswrd  11493  pfxpfx  11496  ccatopth2  11505  pfxccatin12lem4  11514  pfxccatin12lem1  11516  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  pfxccatpfx1  11524  pfxccatpfx2  11525  s3fv0g  11579  s3fv1g  11580  s3fv2g  11581  shftval2  11607  mulreap  11645  elicc4abs  11877  abssubge0  11885  abssuble0  11886  maxleast  11996  maxltsup  12001  xrmaxltsup  12043  xrmineqinf  12054  xrltmininf  12055  xrlemininf  12056  fsumdifsnconst  12241  prodfap0  12331  prodfrecap  12332  fprodabs  12402  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  dvdscmul  12604  summodnegmod  12608  modmulconst  12609  dvdsleabs  12631  dvdsleabs2  12632  addmodlteqALT  12645  dvdsexp  12647  mulmoddvds  12649  divalgb  12711  divgcdz  12767  gcdass  12811  mulgcdr  12814  gcddiv  12815  uzwodc  12833  lcmass  12882  coprmdvds  12889  qredeq  12893  qredeu  12894  congr  12897  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  isprm3  12915  dvdsnprmd  12922  euclemma  12944  prmdvdsexpb  12947  prmexpb  12949  rpexp  12951  znege1  12977  modprminv  13051  modprminveq  13052  vfermltl  13053  modprm0  13056  modprmn0modprm0  13058  coprimeprodsq  13059  coprimeprodsq2  13060  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem6  13072  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem16  13081  pythagtriplem19  13084  pythagtrip  13085  pcmul  13103  pcdiv  13104  pcqcl  13108  pcgcd1  13130  pcgcd  13131  dvdsprmpweq  13137  difsqpwdvds  13140  pcfaclem  13151  ballotfilemsgt1  13306  ballotfilemrv1  13316  ballotfilemrv2  13317  ballotfilemfrcn0  13325  unbendc  13397  strle3g  13515  ercpbl  13705  grpinvid1  13910  grpinvid2  13911  grpasscan1  13921  grpasscan2  13922  grpidrcan  13923  grpidlcan  13924  grpinvadd  13936  grpsubadd  13946  grppncan  13949  qussub  14093  subcmnd  14221  pwsinvg  14299  rng1zrlem  14342  mulgass2  14447  dvrcan1  14531  dvrcan3  14532  rmodislmodlem  14771  rmodislmod  14772  islssm  14778  lsselg  14782  lspss  14820  lspssp  14824  lsslsp  14850  islidlm  14900  lidlnegcl  14906  lidlsubcl  14908  zndvds  15068  assa2ass  15093  assa2ass2  15094  aspss  15103  basgen  15272  clsss  15310  ntrin  15316  ntrcls0  15323  neiint  15337  neiss  15342  neipsm  15346  opnssneib  15348  innei  15355  restco  15366  iscnp  15391  cnconst2  15425  txcn  15467  psmetsym  15521  psmetlecl  15526  distspace  15527  xmetlecl  15559  xmetsym  15560  xblcntrps  15605  xblcntr  15606  blssec  15630  blpnfctr  15631  txmetcn  15711  cnmet  15722  dvid  15887  dvidre  15889  dvply1  15957  ptolemy  16017  sinq12gt0  16023  sincosq1eq  16032  rpcxpsub  16105  relogbexpap  16155  logbleb  16158  logblt  16159  rplogbcxp  16160  lgsval4  16305  lgsmod  16311  lgsne0  16323  lgsmulsqcoprm  16331  2lgsoddprmlem1  16390  structiedg0val  16447  lpvtx  16486  upgredg2vtx  16555  upgredgpr  16556  ushgredgedg  16633  ushgredgedgloop  16635  usgr2v1e2w  16653  wlkeq  16761  clwwlkccatlem  16807  clwwlkccat  16808  clwwlkext2edg  16829  clwwlknccat  16830  s2elclwwlknon2  16843  clwwlknonex2lem2  16845  repiecele0  17241  repiecege0  17242