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  2814  eqeu  2934  tpssi  3790  issod  4355  sotricim  4359  soinxp  4734  funopg  5293  fnco  5369  resasplitss  5440  resdif  5529  fnimapr  5624  ftpg  5749  fsnunfv  5766  fvpr1g  5771  fvpr2g  5772  f1ocnvfvb  5830  f1oiso2  5877  moriotass  5909  f1ofveu  5913  acexmid  5924  ovig  6048  ov6g  6065  ovg  6066  ot1stg  6219  ot2ndg  6220  poxp  6299  brtposg  6321  smores3  6360  smoiso  6369  rdgivallem  6448  frecsuclem  6473  nnaord  6576  nnaword  6578  nnawordex  6596  ecopovtrn  6700  ecopovtrng  6703  xpdom3m  6902  mapxpen  6918  sbthlemi4  7035  djuenun  7297  netap  7339  2omotaplemap  7342  ltsopi  7406  addcanpig  7420  distrnqg  7473  ltsonq  7484  ltanqg  7486  ltmnqg  7487  nnanq0  7544  distrnq0  7545  distnq0r  7549  prarloclem  7587  genpassl  7610  genpassu  7611  distrlem1prl  7668  distrlem1pru  7669  distrlem5prl  7672  distrlem5pru  7673  1idprl  7676  1idpru  7677  ltpopr  7681  ltsopr  7682  ltexprlemm  7686  ltexprlemfl  7695  ltexprlemfu  7697  addcanprlemu  7701  recexprlem1ssl  7719  recexprlem1ssu  7720  aptipr  7727  lttrsr  7848  ltsosr  7850  ltasrg  7856  recexgt0sr  7859  mulextsr1  7867  axmulass  7959  ltxrlt  8111  axltwlin  8113  axlttrn  8114  axltadd  8115  letr  8128  mul12  8174  add12  8203  subadd  8248  addsub  8256  npncan  8266  nppcan  8267  nnpcan  8268  nppcan3  8269  pnpcan  8284  pnncan  8286  ppncan  8287  subdi  8430  ltaddsub2  8483  leaddsub2  8485  ltaddsublt  8617  apreap  8633  lemul1  8639  reapmul1lem  8640  reapadd1  8642  reapcotr  8644  receuap  8715  divassap  8736  div23ap  8737  divmulassap  8741  divmulasscomap  8742  divcanap4  8745  divsubdirap  8754  divcanap5  8760  divdiv32ap  8766  divdivap2  8770  div2subap  8883  letrp1  8894  ltmulgt12  8911  lediv1  8915  ltdiv2  8933  lediv2  8937  lbinfle  8996  difgtsumgt  9414  xrletr  9902  xrre2  9915  xaddass  9963  ixxdisj  9997  ubioc1  10023  lbico1  10024  elioo5  10027  iccsupr  10060  lbicc2  10078  ubicc2  10079  iccneg  10083  icoshft  10084  icodisj  10086  iccf1o  10098  iccen  10100  zltaddlt1le  10101  fztri3or  10133  fzdcel  10134  fzen  10137  uzsubsubfz  10141  fzrevral2  10200  fzshftral  10202  fz0fzdiffz0  10224  difelfznle  10229  fzo1fzo0n0  10278  fzonmapblen  10282  fzosubel2  10290  ubmelfzo  10295  elfzodifsumelfzo  10296  ssfzo12bi  10320  ubmelm1fzo  10321  subfzo0  10337  ceiqle  10424  modqid2  10462  zmodidfzoimp  10465  addmodidr  10484  modfzo0difsn  10506  addmodlteq  10509  frec2uzf1od  10517  exprecap  10691  expdivap  10701  expubnd  10707  sqdivap  10714  mulbinom2  10767  bernneq2  10772  mulsubdivbinom2ap  10822  bcval3  10862  bccmpl  10865  omgadd  10913  shftval2  11010  mulreap  11048  elicc4abs  11278  abssubge0  11286  abssuble0  11287  maxleast  11397  maxltsup  11402  xrmaxltsup  11442  xrmineqinf  11453  xrltmininf  11454  xrlemininf  11455  fsumdifsnconst  11639  prodfap0  11729  prodfrecap  11730  fprodabs  11800  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  dvdscmul  12002  summodnegmod  12006  modmulconst  12007  dvdsleabs  12029  dvdsleabs2  12030  addmodlteqALT  12043  dvdsexp  12045  mulmoddvds  12047  divalgb  12109  divgcdz  12165  gcdass  12209  mulgcdr  12212  gcddiv  12213  uzwodc  12231  lcmass  12280  coprmdvds  12287  qredeq  12291  qredeu  12292  congr  12295  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  isprm3  12313  dvdsnprmd  12320  euclemma  12341  prmdvdsexpb  12344  prmexpb  12346  rpexp  12348  znege1  12373  modprminv  12445  modprminveq  12446  vfermltl  12447  modprm0  12450  modprmn0modprm0  12452  coprimeprodsq  12453  coprimeprodsq2  12454  pythagtriplem1  12461  pythagtriplem3  12463  pythagtriplem6  12466  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem16  12475  pythagtriplem19  12478  pythagtrip  12479  pcmul  12497  pcdiv  12498  pcqcl  12502  pcgcd1  12524  pcgcd  12525  dvdsprmpweq  12531  difsqpwdvds  12534  pcfaclem  12545  unbendc  12698  strle3g  12813  ercpbl  13035  grpinvid1  13256  grpinvid2  13257  grpasscan1  13267  grpasscan2  13268  grpidrcan  13269  grpidlcan  13270  grpinvadd  13282  grpsubadd  13292  grppncan  13295  pwsinvg  13316  qussub  13445  subcmnd  13541  mulgass2  13692  dvrcan1  13774  dvrcan3  13775  rmodislmodlem  13984  rmodislmod  13985  islssm  13991  lsselg  13995  lspss  14033  lspssp  14037  lsslsp  14063  islidlm  14113  lidlnegcl  14119  lidlsubcl  14121  zndvds  14283  basgen  14424  clsss  14462  ntrin  14468  ntrcls0  14475  neiint  14489  neiss  14494  neipsm  14498  opnssneib  14500  innei  14507  restco  14518  iscnp  14543  cnconst2  14577  txcn  14619  psmetsym  14673  psmetlecl  14678  distspace  14679  xmetlecl  14711  xmetsym  14712  xblcntrps  14757  xblcntr  14758  blssec  14782  blpnfctr  14783  txmetcn  14863  cnmet  14874  dvid  15039  dvidre  15041  dvply1  15109  ptolemy  15168  sinq12gt0  15174  sincosq1eq  15183  rpcxpsub  15252  relogbexpap  15302  logbleb  15305  logblt  15306  rplogbcxp  15307  lgsval4  15369  lgsmod  15375  lgsne0  15387  lgsmulsqcoprm  15395  2lgsoddprmlem1  15454