Theorem 3adant3 1043

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

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

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 1006

This theorem is referenced by:  stoic4a  1476  stoic4b  1477  vtoclgft  2854  eqeu  2976  ssprsseq  3835  tpssi  3842  issod  4416  sotricim  4420  soinxp  4796  funopg  5360  fnco  5440  resasplitss  5516  resdif  5605  fnimapr  5706  ftpg  5838  fsnunfv  5855  fvpr1g  5860  fvpr2g  5861  f1ocnvfvb  5921  f1oiso2  5968  moriotass  6002  f1ofveu  6006  acexmid  6017  ovig  6143  ov6g  6160  ovg  6161  ot1stg  6315  ot2ndg  6316  poxp  6397  brtposg  6420  smores3  6459  smoiso  6468  rdgivallem  6547  frecsuclem  6572  nnaord  6677  nnaword  6679  nnawordex  6697  ecopovtrn  6801  ecopovtrng  6804  xpdom3m  7018  mapxpen  7034  sbthlemi4  7159  djuenun  7427  netap  7473  2omotaplemap  7476  ltsopi  7540  addcanpig  7554  distrnqg  7607  ltsonq  7618  ltanqg  7620  ltmnqg  7621  nnanq0  7678  distrnq0  7679  distnq0r  7683  prarloclem  7721  genpassl  7744  genpassu  7745  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  1idprl  7810  1idpru  7811  ltpopr  7815  ltsopr  7816  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  addcanprlemu  7835  recexprlem1ssl  7853  recexprlem1ssu  7854  aptipr  7861  lttrsr  7982  ltsosr  7984  ltasrg  7990  recexgt0sr  7993  mulextsr1  8001  axmulass  8093  ltxrlt  8245  axltwlin  8247  axlttrn  8248  axltadd  8249  letr  8262  mul12  8308  add12  8337  subadd  8382  addsub  8390  npncan  8400  nppcan  8401  nnpcan  8402  nppcan3  8403  pnpcan  8418  pnncan  8420  ppncan  8421  subdi  8564  ltaddsub2  8617  leaddsub2  8619  ltaddsublt  8751  apreap  8767  lemul1  8773  reapmul1lem  8774  reapadd1  8776  reapcotr  8778  receuap  8849  divassap  8870  div23ap  8871  divmulassap  8875  divmulasscomap  8876  divcanap4  8879  divsubdirap  8888  divcanap5  8894  divdiv32ap  8900  divdivap2  8904  div2subap  9017  letrp1  9028  ltmulgt12  9045  lediv1  9049  ltdiv2  9067  lediv2  9071  lbinfle  9130  difgtsumgt  9549  xrletr  10043  xrre2  10056  xaddass  10104  ixxdisj  10138  ubioc1  10164  lbico1  10165  elioo5  10168  iccsupr  10201  lbicc2  10219  ubicc2  10220  iccneg  10224  icoshft  10225  icodisj  10227  iccf1o  10239  iccen  10241  zltaddlt1le  10242  fztri3or  10274  fzdcel  10275  fzen  10278  uzsubsubfz  10282  fzrevral2  10341  fzshftral  10343  fz0fzdiffz0  10365  difelfznle  10370  fzo1fzo0n0  10423  fzonmapblen  10427  fzosubel2  10441  ubmelfzo  10446  elfzodifsumelfzo  10447  ssfzo12bi  10471  ubmelm1fzo  10472  subfzo0  10489  ceiqle  10576  modqid2  10614  zmodidfzoimp  10617  addmodidr  10636  modfzo0difsn  10658  addmodlteq  10661  frec2uzf1od  10669  exprecap  10843  expdivap  10853  expubnd  10859  sqdivap  10866  mulbinom2  10919  bernneq2  10924  mulsubdivbinom2ap  10974  bcval3  11014  bccmpl  11017  omgadd  11066  ccatval1  11178  ccatval2  11179  ccatass  11189  lswccatn0lsw  11192  ccatws1lenp1bg  11216  ccatw2s1leng  11219  pfxfv  11269  pfxnd  11274  pfxtrcfv  11278  pfxsuffeqwrdeq  11283  swrdswrd  11290  pfxpfx  11293  ccatopth2  11302  pfxccatin12lem4  11311  pfxccatin12lem1  11313  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  shftval2  11391  mulreap  11429  elicc4abs  11659  abssubge0  11667  abssuble0  11668  maxleast  11778  maxltsup  11783  xrmaxltsup  11823  xrmineqinf  11834  xrltmininf  11835  xrlemininf  11836  fsumdifsnconst  12021  prodfap0  12111  prodfrecap  12112  fprodabs  12182  sin01gt0  12328  cos01gt0  12329  sin02gt0  12330  dvdscmul  12384  summodnegmod  12388  modmulconst  12389  dvdsleabs  12411  dvdsleabs2  12412  addmodlteqALT  12425  dvdsexp  12427  mulmoddvds  12429  divalgb  12491  divgcdz  12547  gcdass  12591  mulgcdr  12594  gcddiv  12595  uzwodc  12613  lcmass  12662  coprmdvds  12669  qredeq  12673  qredeu  12674  congr  12677  divgcdcoprm0  12678  divgcdcoprmex  12679  cncongr1  12680  cncongr2  12681  isprm3  12695  dvdsnprmd  12702  euclemma  12723  prmdvdsexpb  12726  prmexpb  12728  rpexp  12730  znege1  12755  modprminv  12827  modprminveq  12828  vfermltl  12829  modprm0  12832  modprmn0modprm0  12834  coprimeprodsq  12835  coprimeprodsq2  12836  pythagtriplem1  12843  pythagtriplem3  12845  pythagtriplem6  12848  pythagtriplem12  12853  pythagtriplem13  12854  pythagtriplem14  12855  pythagtriplem16  12857  pythagtriplem19  12860  pythagtrip  12861  pcmul  12879  pcdiv  12880  pcqcl  12884  pcgcd1  12906  pcgcd  12907  dvdsprmpweq  12913  difsqpwdvds  12916  pcfaclem  12927  unbendc  13080  strle3g  13196  ercpbl  13419  grpinvid1  13640  grpinvid2  13641  grpasscan1  13651  grpasscan2  13652  grpidrcan  13653  grpidlcan  13654  grpinvadd  13666  grpsubadd  13676  grppncan  13679  pwsinvg  13700  qussub  13829  subcmnd  13925  mulgass2  14077  dvrcan1  14160  dvrcan3  14161  rmodislmodlem  14370  rmodislmod  14371  islssm  14377  lsselg  14381  lspss  14419  lspssp  14423  lsslsp  14449  islidlm  14499  lidlnegcl  14505  lidlsubcl  14507  zndvds  14669  basgen  14810  clsss  14848  ntrin  14854  ntrcls0  14861  neiint  14875  neiss  14880  neipsm  14884  opnssneib  14886  innei  14893  restco  14904  iscnp  14929  cnconst2  14963  txcn  15005  psmetsym  15059  psmetlecl  15064  distspace  15065  xmetlecl  15097  xmetsym  15098  xblcntrps  15143  xblcntr  15144  blssec  15168  blpnfctr  15169  txmetcn  15249  cnmet  15260  dvid  15425  dvidre  15427  dvply1  15495  ptolemy  15554  sinq12gt0  15560  sincosq1eq  15569  rpcxpsub  15638  relogbexpap  15688  logbleb  15691  logblt  15692  rplogbcxp  15693  lgsval4  15755  lgsmod  15761  lgsne0  15773  lgsmulsqcoprm  15781  2lgsoddprmlem1  15840  structiedg0val  15897  lpvtx  15936  upgredg2vtx  16005  upgredgpr  16006  ushgredgedg  16083  ushgredgedgloop  16085  usgr2v1e2w  16103  wlkeq  16211  clwwlkccatlem  16257  clwwlkccat  16258  clwwlkext2edg  16279  clwwlknccat  16280  s2elclwwlknon2  16293  clwwlknonex2lem2  16295