Theorem 3adant1 1017

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 998	. 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  ax-ia2 107  ax-ia3 108

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

This theorem is referenced by:  3ad2ant2  1021  3ad2ant3  1022  rsp2e  2548  sbciegft  3020  reuhyp  4508  suc11g  4594  soinxp  4734  breldmg  4873  funopg  5293  funimaexglem  5342  fex2  5429  fnreseql  5675  ftpg  5749  mpoeq3ia  5991  funexw  6178  mpofvex  6272  poxp  6299  smores3  6360  tfrlemibxssdm  6394  nndi  6553  nnmass  6554  nndir  6557  fnsnsplitdc  6572  nnaord  6576  nnaordr  6577  nnawordi  6582  nnmord  6584  ecopovtrn  6700  ecopovtrng  6703  ixpf  6788  mapxpen  6918  netap  7339  2omotaplemap  7342  ltsopi  7406  addassnqg  7468  ltsonq  7484  ltmnqg  7487  distrnq0  7545  addlocpr  7622  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  ltpopr  7681  ltsopr  7682  addcanprg  7702  lttrsr  7848  ltsosr  7850  ltasrg  7856  recexgt0sr  7859  mulextsr1lem  7866  mulextsr1  7867  axpre-mulext  7974  adddir  8036  axltwlin  8113  axlttrn  8114  ltleletr  8127  letr  8128  mul32  8175  mul31  8176  add32  8204  subsub23  8250  addsubass  8255  subcan2  8270  subsub2  8273  nppcan2  8276  sub32  8279  nnncan  8280  nnncan2  8282  pnpcan2  8285  subdi  8430  subdir  8431  reapcotr  8644  receuap  8715  divmulap3  8723  divrecap  8734  divrecap2  8735  divsubdirap  8754  divdivap1  8769  redivclap  8777  div2negap  8781  ltmul2  8902  lemul2  8903  lemul2a  8905  lediv1  8915  gt0div  8916  ge0div  8917  ltdivmul  8922  ltdivmul2  8924  ledivmul2  8926  uzind2  9457  nn0ind  9459  fnn0ind  9461  uz3m2nn  9666  xrletr  9902  xrre2  9915  xleadd2a  9968  xleadd1  9969  xltadd2  9971  ixxdisj  9997  iooneg  10082  iccneg  10083  icoshft  10084  icoshftf1o  10085  icodisj  10086  fzen  10137  fzrev3  10181  2ffzeq  10235  fzoaddel2  10288  elfzodifsumelfzo  10296  ssfzo12bi  10320  fzoshftral  10333  adddivflid  10401  fldiv4p1lem1div2  10414  modqmulnn  10453  modqeqmodmin  10505  frec2uzf1od  10517  expdivap  10701  shftval2  11010  mulreap  11048  absdivap  11254  absdiflt  11276  absdifle  11277  abs3dif  11289  cau3  11299  ltmininf  11419  xrmaxlesup  11443  xrltmininf  11454  xrlemininf  11455  xrminltinf  11456  geoisum1c  11704  dvdsmulc  12003  dvdsmultr1  12015  dvdsmultr2  12017  dvdssub2  12019  oexpneg  12061  divalgb  12109  ndvdsadd  12115  gcdaddm  12178  modgcd  12185  dvdsgcd  12206  dvdsgcdb  12207  gcdass  12209  mulgcd  12210  absmulgcd  12211  rpmulgcd  12220  nn0seqcvgd  12236  algcvga  12246  lcmdvds  12274  lcmdvdsb  12279  lcmass  12280  coprmdvds  12287  coprmdvds2  12288  rpmul  12293  cncongr1  12298  cncongr2  12299  prmgt1  12327  qnumdenbi  12387  coprimeprodsq  12453  pythagtriplem4  12464  pythagtriplem8  12468  pythagtriplem9  12469  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pcpremul  12489  pcgcd  12525  setsvala  12736  setsex  12737  ressval2  12771  isgrpi  13228  grpsubrcan  13285  grpinvsub  13286  grpsubeq0  13290  grpsubadd0sub  13291  grpnpcan  13296  qussub  13445  ghmsub  13459  opprmulg  13705  rrgeq0  13899  lmodvsubval2  13976  rmodislmodlem  13984  rmodislmod  13985  lssintclm  14018  lssincl  14019  rnglidlmmgm  14130  cncrng  14203  unopn  14327  clsss  14440  opnssneib  14478  restabs  14497  upxp  14594  blpnfctr  14761  mscl  14787  xmscl  14788  xmsge0  14789  xmseq0  14790  mpomulcn  14888  rpdivcxp  15233  cxpcom  15260  rplogbreexp  15275  rplogbzexp  15276  rprelogbmulexp  15278  logbleb  15283  logblt  15284  lgsneg  15351  lgsne0  15365  lgsmodeq  15372  lgsmulsqcoprm  15373  gausslemma2dlem1a  15385  bj-peano4  15687