Theorem 3adant3 1019

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

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

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 982

This theorem is referenced by:  stoic4a  1443  stoic4b  1444  vtoclgft  2802  eqeu  2922  tpssi  3774  issod  4337  sotricim  4341  soinxp  4714  funopg  5269  fnco  5343  resasplitss  5414  resdif  5502  fnimapr  5597  ftpg  5721  fsnunfv  5738  fvpr1g  5743  fvpr2g  5744  f1ocnvfvb  5802  f1oiso2  5849  moriotass  5880  f1ofveu  5884  acexmid  5895  ovig  6018  ov6g  6034  ovg  6035  ot1stg  6177  ot2ndg  6178  poxp  6257  brtposg  6279  smores3  6318  smoiso  6327  rdgivallem  6406  frecsuclem  6431  nnaord  6534  nnaword  6536  nnawordex  6554  ecopovtrn  6658  ecopovtrng  6661  xpdom3m  6860  mapxpen  6876  sbthlemi4  6989  djuenun  7241  netap  7283  2omotaplemap  7286  ltsopi  7349  addcanpig  7363  distrnqg  7416  ltsonq  7427  ltanqg  7429  ltmnqg  7430  nnanq0  7487  distrnq0  7488  distnq0r  7492  prarloclem  7530  genpassl  7553  genpassu  7554  distrlem1prl  7611  distrlem1pru  7612  distrlem5prl  7615  distrlem5pru  7616  1idprl  7619  1idpru  7620  ltpopr  7624  ltsopr  7625  ltexprlemm  7629  ltexprlemfl  7638  ltexprlemfu  7640  addcanprlemu  7644  recexprlem1ssl  7662  recexprlem1ssu  7663  aptipr  7670  lttrsr  7791  ltsosr  7793  ltasrg  7799  recexgt0sr  7802  mulextsr1  7810  axmulass  7902  ltxrlt  8053  axltwlin  8055  axlttrn  8056  axltadd  8057  letr  8070  mul12  8116  add12  8145  subadd  8190  addsub  8198  npncan  8208  nppcan  8209  nnpcan  8210  nppcan3  8211  pnpcan  8226  pnncan  8228  ppncan  8229  subdi  8372  ltaddsub2  8424  leaddsub2  8426  ltaddsublt  8558  apreap  8574  lemul1  8580  reapmul1lem  8581  reapadd1  8583  reapcotr  8585  receuap  8656  divassap  8677  div23ap  8678  divmulassap  8682  divmulasscomap  8683  divcanap4  8686  divsubdirap  8695  divcanap5  8701  divdiv32ap  8707  divdivap2  8711  div2subap  8824  letrp1  8835  ltmulgt12  8852  lediv1  8856  ltdiv2  8874  lediv2  8878  lbinfle  8937  difgtsumgt  9352  xrletr  9838  xrre2  9851  xaddass  9899  ixxdisj  9933  ubioc1  9959  lbico1  9960  elioo5  9963  iccsupr  9996  lbicc2  10014  ubicc2  10015  iccneg  10019  icoshft  10020  icodisj  10022  iccf1o  10034  iccen  10036  zltaddlt1le  10037  fztri3or  10069  fzdcel  10070  fzen  10073  uzsubsubfz  10077  fzrevral2  10136  fzshftral  10138  fz0fzdiffz0  10160  difelfznle  10165  fzo1fzo0n0  10213  fzonmapblen  10217  fzosubel2  10225  ubmelfzo  10230  elfzodifsumelfzo  10231  ssfzo12bi  10255  ubmelm1fzo  10256  subfzo0  10272  ceiqle  10344  modqid2  10382  zmodidfzoimp  10385  addmodidr  10404  modfzo0difsn  10426  addmodlteq  10429  frec2uzf1od  10437  exprecap  10592  expdivap  10602  expubnd  10608  sqdivap  10615  mulbinom2  10668  bernneq2  10673  mulsubdivbinom2ap  10723  bcval3  10763  bccmpl  10766  omgadd  10814  shftval2  10867  mulreap  10905  elicc4abs  11135  abssubge0  11143  abssuble0  11144  maxleast  11254  maxltsup  11259  xrmaxltsup  11298  xrmineqinf  11309  xrltmininf  11310  xrlemininf  11311  fsumdifsnconst  11495  prodfap0  11585  prodfrecap  11586  fprodabs  11656  sin01gt0  11801  cos01gt0  11802  sin02gt0  11803  dvdscmul  11857  summodnegmod  11861  modmulconst  11862  dvdsleabs  11883  dvdsleabs2  11884  addmodlteqALT  11897  dvdsexp  11899  mulmoddvds  11901  divalgb  11962  divgcdz  12004  gcdass  12048  mulgcdr  12051  gcddiv  12052  uzwodc  12070  lcmass  12117  coprmdvds  12124  qredeq  12128  qredeu  12129  congr  12132  divgcdcoprm0  12133  divgcdcoprmex  12134  cncongr1  12135  cncongr2  12136  isprm3  12150  dvdsnprmd  12157  euclemma  12178  prmdvdsexpb  12181  prmexpb  12183  rpexp  12185  znege1  12210  modprminv  12281  modprminveq  12282  vfermltl  12283  modprm0  12286  modprmn0modprm0  12288  coprimeprodsq  12289  coprimeprodsq2  12290  pythagtriplem1  12297  pythagtriplem3  12299  pythagtriplem6  12302  pythagtriplem12  12307  pythagtriplem13  12308  pythagtriplem14  12309  pythagtriplem16  12311  pythagtriplem19  12314  pythagtrip  12315  pcmul  12333  pcdiv  12334  pcqcl  12338  pcgcd1  12360  pcgcd  12361  dvdsprmpweq  12367  difsqpwdvds  12370  pcfaclem  12381  unbendc  12505  strle3g  12620  ercpbl  12807  grpinvid1  12996  grpinvid2  12997  grpasscan1  13007  grpasscan2  13008  grpidrcan  13009  grpidlcan  13010  grpinvadd  13022  grpsubadd  13032  grppncan  13035  qussub  13176  subcmnd  13270  mulgass2  13410  dvrcan1  13490  dvrcan3  13491  rmodislmodlem  13666  rmodislmod  13667  islssm  13673  lsselg  13677  lspss  13715  lspssp  13719  lsslsp  13745  islidlm  13795  lidlnegcl  13801  lidlsubcl  13803  basgen  14037  clsss  14075  ntrin  14081  ntrcls0  14088  neiint  14102  neiss  14107  neipsm  14111  opnssneib  14113  innei  14120  restco  14131  iscnp  14156  cnconst2  14190  txcn  14232  psmetsym  14286  psmetlecl  14291  distspace  14292  xmetlecl  14324  xmetsym  14325  xblcntrps  14370  xblcntr  14371  blssec  14395  blpnfctr  14396  txmetcn  14476  cnmet  14487  dvid  14619  ptolemy  14702  sinq12gt0  14708  sincosq1eq  14717  rpcxpsub  14786  relogbexpap  14833  logbleb  14836  logblt  14837  rplogbcxp  14838  lgsval4  14879  lgsmod  14885  lgsne0  14897  lgsmulsqcoprm  14905  2lgsoddprmlem1  14911