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  5837  fsnunfv  5854  fvpr1g  5859  fvpr2g  5860  f1ocnvfvb  5920  f1oiso2  5967  moriotass  6001  f1ofveu  6005  acexmid  6016  ovig  6142  ov6g  6159  ovg  6160  ot1stg  6314  ot2ndg  6315  poxp  6396  brtposg  6419  smores3  6458  smoiso  6467  rdgivallem  6546  frecsuclem  6571  nnaord  6676  nnaword  6678  nnawordex  6696  ecopovtrn  6800  ecopovtrng  6803  xpdom3m  7017  mapxpen  7033  sbthlemi4  7158  djuenun  7426  netap  7472  2omotaplemap  7475  ltsopi  7539  addcanpig  7553  distrnqg  7606  ltsonq  7617  ltanqg  7619  ltmnqg  7620  nnanq0  7677  distrnq0  7678  distnq0r  7682  prarloclem  7720  genpassl  7743  genpassu  7744  distrlem1prl  7801  distrlem1pru  7802  distrlem5prl  7805  distrlem5pru  7806  1idprl  7809  1idpru  7810  ltpopr  7814  ltsopr  7815  ltexprlemm  7819  ltexprlemfl  7828  ltexprlemfu  7830  addcanprlemu  7834  recexprlem1ssl  7852  recexprlem1ssu  7853  aptipr  7860  lttrsr  7981  ltsosr  7983  ltasrg  7989  recexgt0sr  7992  mulextsr1  8000  axmulass  8092  ltxrlt  8244  axltwlin  8246  axlttrn  8247  axltadd  8248  letr  8261  mul12  8307  add12  8336  subadd  8381  addsub  8389  npncan  8399  nppcan  8400  nnpcan  8401  nppcan3  8402  pnpcan  8417  pnncan  8419  ppncan  8420  subdi  8563  ltaddsub2  8616  leaddsub2  8618  ltaddsublt  8750  apreap  8766  lemul1  8772  reapmul1lem  8773  reapadd1  8775  reapcotr  8777  receuap  8848  divassap  8869  div23ap  8870  divmulassap  8874  divmulasscomap  8875  divcanap4  8878  divsubdirap  8887  divcanap5  8893  divdiv32ap  8899  divdivap2  8903  div2subap  9016  letrp1  9027  ltmulgt12  9044  lediv1  9048  ltdiv2  9066  lediv2  9070  lbinfle  9129  difgtsumgt  9548  xrletr  10042  xrre2  10055  xaddass  10103  ixxdisj  10137  ubioc1  10163  lbico1  10164  elioo5  10167  iccsupr  10200  lbicc2  10218  ubicc2  10219  iccneg  10223  icoshft  10224  icodisj  10226  iccf1o  10238  iccen  10240  zltaddlt1le  10241  fztri3or  10273  fzdcel  10274  fzen  10277  uzsubsubfz  10281  fzrevral2  10340  fzshftral  10342  fz0fzdiffz0  10364  difelfznle  10369  fzo1fzo0n0  10421  fzonmapblen  10425  fzosubel2  10439  ubmelfzo  10444  elfzodifsumelfzo  10445  ssfzo12bi  10469  ubmelm1fzo  10470  subfzo0  10487  ceiqle  10574  modqid2  10612  zmodidfzoimp  10615  addmodidr  10634  modfzo0difsn  10656  addmodlteq  10659  frec2uzf1od  10667  exprecap  10841  expdivap  10851  expubnd  10857  sqdivap  10864  mulbinom2  10917  bernneq2  10922  mulsubdivbinom2ap  10972  bcval3  11012  bccmpl  11015  omgadd  11064  ccatval1  11173  ccatval2  11174  ccatass  11184  lswccatn0lsw  11187  ccatws1lenp1bg  11211  ccatw2s1leng  11214  pfxfv  11264  pfxnd  11269  pfxtrcfv  11273  pfxsuffeqwrdeq  11278  swrdswrd  11285  pfxpfx  11288  ccatopth2  11297  pfxccatin12lem4  11306  pfxccatin12lem1  11308  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  pfxccatpfx1  11316  pfxccatpfx2  11317  s3fv0g  11371  s3fv1g  11372  s3fv2g  11373  shftval2  11386  mulreap  11424  elicc4abs  11654  abssubge0  11662  abssuble0  11663  maxleast  11773  maxltsup  11778  xrmaxltsup  11818  xrmineqinf  11829  xrltmininf  11830  xrlemininf  11831  fsumdifsnconst  12015  prodfap0  12105  prodfrecap  12106  fprodabs  12176  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  dvdscmul  12378  summodnegmod  12382  modmulconst  12383  dvdsleabs  12405  dvdsleabs2  12406  addmodlteqALT  12419  dvdsexp  12421  mulmoddvds  12423  divalgb  12485  divgcdz  12541  gcdass  12585  mulgcdr  12588  gcddiv  12589  uzwodc  12607  lcmass  12656  coprmdvds  12663  qredeq  12667  qredeu  12668  congr  12671  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  isprm3  12689  dvdsnprmd  12696  euclemma  12717  prmdvdsexpb  12720  prmexpb  12722  rpexp  12724  znege1  12749  modprminv  12821  modprminveq  12822  vfermltl  12823  modprm0  12826  modprmn0modprm0  12828  coprimeprodsq  12829  coprimeprodsq2  12830  pythagtriplem1  12837  pythagtriplem3  12839  pythagtriplem6  12842  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem16  12851  pythagtriplem19  12854  pythagtrip  12855  pcmul  12873  pcdiv  12874  pcqcl  12878  pcgcd1  12900  pcgcd  12901  dvdsprmpweq  12907  difsqpwdvds  12910  pcfaclem  12921  unbendc  13074  strle3g  13190  ercpbl  13413  grpinvid1  13634  grpinvid2  13635  grpasscan1  13645  grpasscan2  13646  grpidrcan  13647  grpidlcan  13648  grpinvadd  13660  grpsubadd  13670  grppncan  13673  pwsinvg  13694  qussub  13823  subcmnd  13919  mulgass2  14070  dvrcan1  14153  dvrcan3  14154  rmodislmodlem  14363  rmodislmod  14364  islssm  14370  lsselg  14374  lspss  14412  lspssp  14416  lsslsp  14442  islidlm  14492  lidlnegcl  14498  lidlsubcl  14500  zndvds  14662  basgen  14803  clsss  14841  ntrin  14847  ntrcls0  14854  neiint  14868  neiss  14873  neipsm  14877  opnssneib  14879  innei  14886  restco  14897  iscnp  14922  cnconst2  14956  txcn  14998  psmetsym  15052  psmetlecl  15057  distspace  15058  xmetlecl  15090  xmetsym  15091  xblcntrps  15136  xblcntr  15137  blssec  15161  blpnfctr  15162  txmetcn  15242  cnmet  15253  dvid  15418  dvidre  15420  dvply1  15488  ptolemy  15547  sinq12gt0  15553  sincosq1eq  15562  rpcxpsub  15631  relogbexpap  15681  logbleb  15684  logblt  15685  rplogbcxp  15686  lgsval4  15748  lgsmod  15754  lgsne0  15766  lgsmulsqcoprm  15774  2lgsoddprmlem1  15833  structiedg0val  15890  lpvtx  15929  upgredg2vtx  15998  upgredgpr  15999  ushgredgedg  16076  ushgredgedgloop  16078  usgr2v1e2w  16096  wlkeq  16204  clwwlkccatlem  16250  clwwlkccat  16251  clwwlkext2edg  16272  clwwlknccat  16273  s2elclwwlknon2  16286  clwwlknonex2lem2  16288