Theorem 3adant3 1044

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

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

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 1007

This theorem is referenced by:  stoic4a  1477  stoic4b  1478  vtoclgft  2855  eqeu  2977  ssprsseq  3840  tpssi  3847  issod  4422  sotricim  4426  soinxp  4802  funopg  5367  fnco  5447  resasplitss  5524  resdif  5614  fnimapr  5715  ftpg  5846  fsnunfv  5863  fvpr1g  5868  fvpr2g  5869  f1ocnvfvb  5931  f1oiso2  5978  moriotass  6012  f1ofveu  6016  acexmid  6027  ovig  6153  ov6g  6170  ovg  6171  ot1stg  6324  ot2ndg  6325  poxp  6406  suppvalfn  6419  suppsnopdc  6428  suppfnss  6435  funsssuppss  6436  brtposg  6463  smores3  6502  smoiso  6511  rdgivallem  6590  frecsuclem  6615  nnaord  6720  nnaword  6722  nnawordex  6740  ecopovtrn  6844  ecopovtrng  6847  xpdom3m  7061  mapxpen  7077  sbthlemi4  7202  djuenun  7470  netap  7516  2omotaplemap  7519  ltsopi  7583  addcanpig  7597  distrnqg  7650  ltsonq  7661  ltanqg  7663  ltmnqg  7664  nnanq0  7721  distrnq0  7722  distnq0r  7726  prarloclem  7764  genpassl  7787  genpassu  7788  distrlem1prl  7845  distrlem1pru  7846  distrlem5prl  7849  distrlem5pru  7850  1idprl  7853  1idpru  7854  ltpopr  7858  ltsopr  7859  ltexprlemm  7863  ltexprlemfl  7872  ltexprlemfu  7874  addcanprlemu  7878  recexprlem1ssl  7896  recexprlem1ssu  7897  aptipr  7904  lttrsr  8025  ltsosr  8027  ltasrg  8033  recexgt0sr  8036  mulextsr1  8044  axmulass  8136  ltxrlt  8287  axltwlin  8289  axlttrn  8290  axltadd  8291  letr  8304  mul12  8350  add12  8379  subadd  8424  addsub  8432  npncan  8442  nppcan  8443  nnpcan  8444  nppcan3  8445  pnpcan  8460  pnncan  8462  ppncan  8463  subdi  8606  ltaddsub2  8659  leaddsub2  8661  ltaddsublt  8793  apreap  8809  lemul1  8815  reapmul1lem  8816  reapadd1  8818  reapcotr  8820  receuap  8891  divassap  8912  div23ap  8913  divmulassap  8917  divmulasscomap  8918  divcanap4  8921  divsubdirap  8930  divcanap5  8936  divdiv32ap  8942  divdivap2  8946  div2subap  9059  letrp1  9070  ltmulgt12  9087  lediv1  9091  ltdiv2  9109  lediv2  9113  lbinfle  9172  difgtsumgt  9593  xrletr  10087  xrre2  10100  xaddass  10148  ixxdisj  10182  ubioc1  10208  lbico1  10209  elioo5  10212  iccsupr  10245  lbicc2  10263  ubicc2  10264  iccneg  10268  icoshft  10269  icodisj  10271  lincmble  10283  iccf1o  10284  iccen  10286  zltaddlt1le  10287  fztri3or  10319  fzdcel  10320  fzen  10323  uzsubsubfz  10327  fzrevral2  10386  fzshftral  10388  fz0fzdiffz0  10410  difelfznle  10415  fzo1fzo0n0  10468  fzonmapblen  10472  fzosubel2  10486  ubmelfzo  10491  elfzodifsumelfzo  10492  ssfzo12bi  10516  ubmelm1fzo  10517  subfzo0  10534  ceiqle  10621  modqid2  10659  zmodidfzoimp  10662  addmodidr  10681  modfzo0difsn  10703  addmodlteq  10706  frec2uzf1od  10714  exprecap  10888  expdivap  10898  expubnd  10904  sqdivap  10911  mulbinom2  10964  bernneq2  10969  mulsubdivbinom2ap  11019  bcval3  11059  bccmpl  11062  omgadd  11111  ccatval1  11223  ccatval2  11224  ccatass  11234  lswccatn0lsw  11237  ccatws1lenp1bg  11261  ccatw2s1leng  11264  pfxfv  11314  pfxnd  11319  pfxtrcfv  11323  pfxsuffeqwrdeq  11328  swrdswrd  11335  pfxpfx  11338  ccatopth2  11347  pfxccatin12lem4  11356  pfxccatin12lem1  11358  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  pfxccatpfx1  11366  pfxccatpfx2  11367  s3fv0g  11421  s3fv1g  11422  s3fv2g  11423  shftval2  11449  mulreap  11487  elicc4abs  11717  abssubge0  11725  abssuble0  11726  maxleast  11836  maxltsup  11841  xrmaxltsup  11881  xrmineqinf  11892  xrltmininf  11893  xrlemininf  11894  fsumdifsnconst  12079  prodfap0  12169  prodfrecap  12170  fprodabs  12240  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  dvdscmul  12442  summodnegmod  12446  modmulconst  12447  dvdsleabs  12469  dvdsleabs2  12470  addmodlteqALT  12483  dvdsexp  12485  mulmoddvds  12487  divalgb  12549  divgcdz  12605  gcdass  12649  mulgcdr  12652  gcddiv  12653  uzwodc  12671  lcmass  12720  coprmdvds  12727  qredeq  12731  qredeu  12732  congr  12735  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  isprm3  12753  dvdsnprmd  12760  euclemma  12781  prmdvdsexpb  12784  prmexpb  12786  rpexp  12788  znege1  12813  modprminv  12885  modprminveq  12886  vfermltl  12887  modprm0  12890  modprmn0modprm0  12892  coprimeprodsq  12893  coprimeprodsq2  12894  pythagtriplem1  12901  pythagtriplem3  12903  pythagtriplem6  12906  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem14  12913  pythagtriplem16  12915  pythagtriplem19  12918  pythagtrip  12919  pcmul  12937  pcdiv  12938  pcqcl  12942  pcgcd1  12964  pcgcd  12965  dvdsprmpweq  12971  difsqpwdvds  12974  pcfaclem  12985  unbendc  13138  strle3g  13254  ercpbl  13477  grpinvid1  13698  grpinvid2  13699  grpasscan1  13709  grpasscan2  13710  grpidrcan  13711  grpidlcan  13712  grpinvadd  13724  grpsubadd  13734  grppncan  13737  pwsinvg  13758  qussub  13887  subcmnd  13983  mulgass2  14135  dvrcan1  14218  dvrcan3  14219  rmodislmodlem  14429  rmodislmod  14430  islssm  14436  lsselg  14440  lspss  14478  lspssp  14482  lsslsp  14508  islidlm  14558  lidlnegcl  14564  lidlsubcl  14566  zndvds  14728  basgen  14874  clsss  14912  ntrin  14918  ntrcls0  14925  neiint  14939  neiss  14944  neipsm  14948  opnssneib  14950  innei  14957  restco  14968  iscnp  14993  cnconst2  15027  txcn  15069  psmetsym  15123  psmetlecl  15128  distspace  15129  xmetlecl  15161  xmetsym  15162  xblcntrps  15207  xblcntr  15208  blssec  15232  blpnfctr  15233  txmetcn  15313  cnmet  15324  dvid  15489  dvidre  15491  dvply1  15559  ptolemy  15618  sinq12gt0  15624  sincosq1eq  15633  rpcxpsub  15702  relogbexpap  15752  logbleb  15755  logblt  15756  rplogbcxp  15757  lgsval4  15822  lgsmod  15828  lgsne0  15840  lgsmulsqcoprm  15848  2lgsoddprmlem1  15907  structiedg0val  15964  lpvtx  16003  upgredg2vtx  16072  upgredgpr  16073  ushgredgedg  16150  ushgredgedgloop  16152  usgr2v1e2w  16170  wlkeq  16278  clwwlkccatlem  16324  clwwlkccat  16325  clwwlkext2edg  16346  clwwlknccat  16347  s2elclwwlknon2  16360  clwwlknonex2lem2  16362  repiecele0  16741  repiecege0  16742