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  7337  2omotaplemap  7340  ltsopi  7404  addassnqg  7466  ltsonq  7482  ltmnqg  7485  distrnq0  7543  addlocpr  7620  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  ltpopr  7679  ltsopr  7680  addcanprg  7700  lttrsr  7846  ltsosr  7848  ltasrg  7854  recexgt0sr  7857  mulextsr1lem  7864  mulextsr1  7865  axpre-mulext  7972  adddir  8034  axltwlin  8111  axlttrn  8112  ltleletr  8125  letr  8126  mul32  8173  mul31  8174  add32  8202  subsub23  8248  addsubass  8253  subcan2  8268  subsub2  8271  nppcan2  8274  sub32  8277  nnncan  8278  nnncan2  8280  pnpcan2  8283  subdi  8428  subdir  8429  reapcotr  8642  receuap  8713  divmulap3  8721  divrecap  8732  divrecap2  8733  divsubdirap  8752  divdivap1  8767  redivclap  8775  div2negap  8779  ltmul2  8900  lemul2  8901  lemul2a  8903  lediv1  8913  gt0div  8914  ge0div  8915  ltdivmul  8920  ltdivmul2  8922  ledivmul2  8924  uzind2  9455  nn0ind  9457  fnn0ind  9459  uz3m2nn  9664  xrletr  9900  xrre2  9913  xleadd2a  9966  xleadd1  9967  xltadd2  9969  ixxdisj  9995  iooneg  10080  iccneg  10081  icoshft  10082  icoshftf1o  10083  icodisj  10084  fzen  10135  fzrev3  10179  2ffzeq  10233  fzoaddel2  10286  elfzodifsumelfzo  10294  ssfzo12bi  10318  fzoshftral  10331  adddivflid  10399  fldiv4p1lem1div2  10412  modqmulnn  10451  modqeqmodmin  10503  frec2uzf1od  10515  expdivap  10699  shftval2  11008  mulreap  11046  absdivap  11252  absdiflt  11274  absdifle  11275  abs3dif  11287  cau3  11297  ltmininf  11417  xrmaxlesup  11441  xrltmininf  11452  xrlemininf  11453  xrminltinf  11454  geoisum1c  11702  dvdsmulc  12001  dvdsmultr1  12013  dvdsmultr2  12015  dvdssub2  12017  oexpneg  12059  divalgb  12107  ndvdsadd  12113  gcdaddm  12176  modgcd  12183  dvdsgcd  12204  dvdsgcdb  12205  gcdass  12207  mulgcd  12208  absmulgcd  12209  rpmulgcd  12218  nn0seqcvgd  12234  algcvga  12244  lcmdvds  12272  lcmdvdsb  12277  lcmass  12278  coprmdvds  12285  coprmdvds2  12286  rpmul  12291  cncongr1  12296  cncongr2  12297  prmgt1  12325  qnumdenbi  12385  coprimeprodsq  12451  pythagtriplem4  12462  pythagtriplem8  12466  pythagtriplem9  12467  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  pcpremul  12487  pcgcd  12523  setsvala  12734  setsex  12735  ressval2  12769  isgrpi  13226  grpsubrcan  13283  grpinvsub  13284  grpsubeq0  13288  grpsubadd0sub  13289  grpnpcan  13294  qussub  13443  ghmsub  13457  opprmulg  13703  rrgeq0  13897  lmodvsubval2  13974  rmodislmodlem  13982  rmodislmod  13983  lssintclm  14016  lssincl  14017  rnglidlmmgm  14128  cncrng  14201  unopn  14325  clsss  14438  opnssneib  14476  restabs  14495  upxp  14592  blpnfctr  14759  mscl  14785  xmscl  14786  xmsge0  14787  xmseq0  14788  mpomulcn  14886  rpdivcxp  15231  cxpcom  15258  rplogbreexp  15273  rplogbzexp  15274  rprelogbmulexp  15276  logbleb  15281  logblt  15282  lgsneg  15349  lgsne0  15363  lgsmodeq  15370  lgsmulsqcoprm  15371  gausslemma2dlem1a  15383  bj-peano4  15685