Theorem 3adant1 1042

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant1	⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 1023	. 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3ad2ant2  1046  3ad2ant3  1047  rsp2e  2584  sbciegft  3063  reuhyp  4575  suc11g  4661  soinxp  4802  breldmg  4943  funopg  5367  funimaexglem  5420  fex2  5511  fnreseql  5766  ftpg  5846  mpoeq3ia  6096  funexw  6283  mpofvex  6379  poxp  6406  suppval1  6417  smores3  6502  tfrlemibxssdm  6536  nndi  6697  nnmass  6698  nndir  6701  fnsnsplitdc  6716  nnaord  6720  nnaordr  6721  nnawordi  6726  nnmord  6728  ecopovtrn  6844  ecopovtrng  6847  ixpf  6932  f1oen4g  6968  f1dom4g  6969  mapxpen  7077  netap  7516  2omotaplemap  7519  ltsopi  7583  addassnqg  7645  ltsonq  7661  ltmnqg  7664  distrnq0  7722  addlocpr  7799  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  ltpopr  7858  ltsopr  7859  addcanprg  7879  lttrsr  8025  ltsosr  8027  ltasrg  8033  recexgt0sr  8036  mulextsr1lem  8043  mulextsr1  8044  axpre-mulext  8151  adddir  8213  axltwlin  8289  axlttrn  8290  ltleletr  8303  letr  8304  mul32  8351  mul31  8352  add32  8380  subsub23  8426  addsubass  8431  subcan2  8446  subsub2  8449  nppcan2  8452  sub32  8455  nnncan  8456  nnncan2  8458  pnpcan2  8461  subdi  8606  subdir  8607  reapcotr  8820  receuap  8891  divmulap3  8899  divrecap  8910  divrecap2  8911  divsubdirap  8930  divdivap1  8945  redivclap  8953  div2negap  8957  ltmul2  9078  lemul2  9079  lemul2a  9081  lediv1  9091  gt0div  9092  ge0div  9093  ltdivmul  9098  ltdivmul2  9100  ledivmul2  9102  uzind2  9636  nn0ind  9638  fnn0ind  9640  uz3m2nn  9851  xrletr  10087  xrre2  10100  xleadd2a  10153  xleadd1  10154  xltadd2  10156  ixxdisj  10182  iooneg  10267  iccneg  10268  icoshft  10269  icoshftf1o  10270  icodisj  10271  fzen  10323  fzrev3  10367  2ffzeq  10421  fzoaddel2  10481  elfzodifsumelfzo  10492  ssfzo12bi  10516  fzoshftral  10530  adddivflid  10598  fldiv4p1lem1div2  10611  modqmulnn  10650  modqeqmodmin  10702  frec2uzf1od  10714  expdivap  10898  ccatval1  11223  ccatass  11234  fzowrddc  11277  swrdval  11278  swrdnd  11289  swrd0g  11290  swrdfv2  11293  pfxsuff1eqwrdeq  11329  swrdswrdlem  11334  pfxccatin12lem2a  11357  pfxccatin12lem1  11358  shftval2  11449  mulreap  11487  absdivap  11693  absdiflt  11715  absdifle  11716  abs3dif  11728  cau3  11738  ltmininf  11858  xrmaxlesup  11882  xrltmininf  11893  xrlemininf  11894  xrminltinf  11895  geoisum1c  12144  dvdsmulc  12443  dvdsmultr1  12455  dvdsmultr2  12457  dvdssub2  12459  oexpneg  12501  divalgb  12549  ndvdsadd  12555  gcdaddm  12618  modgcd  12625  dvdsgcd  12646  dvdsgcdb  12647  gcdass  12649  mulgcd  12650  absmulgcd  12651  rpmulgcd  12660  nn0seqcvgd  12676  algcvga  12686  lcmdvds  12714  lcmdvdsb  12719  lcmass  12720  coprmdvds  12727  coprmdvds2  12728  rpmul  12733  cncongr1  12738  cncongr2  12739  prmgt1  12767  qnumdenbi  12827  coprimeprodsq  12893  pythagtriplem4  12904  pythagtriplem8  12908  pythagtriplem9  12909  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  pcpremul  12929  pcgcd  12965  setsvala  13176  setsex  13177  ressval2  13212  isgrpi  13670  grpsubrcan  13727  grpinvsub  13728  grpsubeq0  13732  grpsubadd0sub  13733  grpnpcan  13738  qussub  13887  ghmsub  13901  opprmulg  14148  rrgeq0  14343  lmodvsubval2  14421  rmodislmodlem  14429  rmodislmod  14430  lssintclm  14463  lssincl  14464  rnglidlmmgm  14575  cncrng  14648  unopn  14799  clsss  14912  opnssneib  14950  restabs  14969  upxp  15066  blpnfctr  15233  mscl  15259  xmscl  15260  xmsge0  15261  xmseq0  15262  mpomulcn  15360  rpdivcxp  15705  cxpcom  15732  rplogbreexp  15747  rplogbzexp  15748  rprelogbmulexp  15750  logbleb  15755  logblt  15756  lgsneg  15826  lgsne0  15840  lgsmodeq  15847  lgsmulsqcoprm  15848  gausslemma2dlem1a  15860  funvtxdm2domval  15953  funiedgdm2domval  15954  iedgedgg  15985  iswlk  16247  uspgr2wlkeq  16289  uspgr2wlkeq2  16290  uspgr2wlkeqi  16291  istrl  16309  clwwlkgt0  16320  iseupth  16371  bj-peano4  16654