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  14349  clsss  14462  opnssneib  14500  restabs  14519  upxp  14616  blpnfctr  14783  mscl  14809  xmscl  14810  xmsge0  14811  xmseq0  14812  mpomulcn  14910  rpdivcxp  15255  cxpcom  15282  rplogbreexp  15297  rplogbzexp  15298  rprelogbmulexp  15300  logbleb  15305  logblt  15306  lgsneg  15373  lgsne0  15387  lgsmodeq  15394  lgsmulsqcoprm  15395  gausslemma2dlem1a  15407  bj-peano4  15709