Theorem 3adant1 980

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 961	. 2 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 943

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  3ad2ant2  984  3ad2ant3  985  rsp2e  2455  sbciegft  2905  reuhyp  4351  suc11g  4430  soinxp  4567  breldmg  4703  funopg  5113  funimaexglem  5162  fex2  5247  fnreseql  5482  ftpg  5556  mpoeq3ia  5788  mpofvex  6052  poxp  6080  smores3  6141  tfrlemibxssdm  6175  nndi  6333  nnmass  6334  nndir  6337  fnsnsplitdc  6352  nnaord  6356  nnaordr  6357  nnawordi  6362  nnmord  6364  ecopovtrn  6477  ecopovtrng  6480  ixpf  6565  mapxpen  6692  ltsopi  7069  addassnqg  7131  ltsonq  7147  ltmnqg  7150  distrnq0  7208  addlocpr  7285  distrlem1prl  7331  distrlem1pru  7332  distrlem4prl  7333  distrlem4pru  7334  ltpopr  7344  ltsopr  7345  addcanprg  7365  lttrsr  7498  ltsosr  7500  ltasrg  7506  recexgt0sr  7509  mulextsr1lem  7515  mulextsr1  7516  axpre-mulext  7616  adddir  7674  axltwlin  7749  axlttrn  7750  ltleletr  7762  letr  7763  mul32  7808  mul31  7809  add32  7837  subsub23  7883  addsubass  7888  subcan2  7903  subsub2  7906  nppcan2  7909  sub32  7912  nnncan  7913  nnncan2  7915  pnpcan2  7918  subdi  8059  subdir  8060  reapcotr  8271  receuap  8336  divmulap3  8343  divrecap  8354  divrecap2  8355  divsubdirap  8374  divdivap1  8389  redivclap  8397  div2negap  8401  ltmul2  8517  lemul2  8518  lemul2a  8520  lediv1  8530  gt0div  8531  ge0div  8532  ltdivmul  8537  ltdivmul2  8539  ledivmul2  8541  uzind2  9060  nn0ind  9062  fnn0ind  9064  uz3m2nn  9263  xrletr  9477  xrre2  9490  xleadd2a  9543  xleadd1  9544  xltadd2  9546  ixxdisj  9572  iooneg  9657  iccneg  9658  icoshft  9659  icoshftf1o  9660  icodisj  9661  fzen  9709  fzrev3  9753  2ffzeq  9804  fzoaddel2  9856  elfzodifsumelfzo  9864  ssfzo12bi  9888  fzoshftral  9901  adddivflid  9951  fldiv4p1lem1div2  9964  modqmulnn  10001  modqeqmodmin  10053  frec2uzf1od  10065  expdivap  10230  shftval2  10484  mulreap  10522  absdivap  10727  absdiflt  10749  absdifle  10750  abs3dif  10762  cau3  10772  ltmininf  10891  xrmaxlesup  10913  xrltmininf  10924  xrlemininf  10925  xrminltinf  10926  geoisum1c  11174  dvdsmulc  11362  dvdsmultr1  11372  dvdsmultr2  11374  dvdssub2  11376  oexpneg  11415  divalgb  11463  ndvdsadd  11469  gcdaddm  11513  modgcd  11520  dvdsgcd  11539  dvdsgcdb  11540  gcdass  11542  mulgcd  11543  absmulgcd  11544  rpmulgcd  11553  nn0seqcvgd  11561  algcvga  11571  lcmdvds  11599  lcmdvdsb  11604  lcmass  11605  coprmdvds  11612  coprmdvds2  11613  rpmul  11618  cncongr1  11623  cncongr2  11624  prmgt1  11651  qnumdenbi  11708  setsvala  11826  setsex  11827  unopn  12008  clsss  12123  opnssneib  12161  restabs  12180  upxp  12276  blpnfctr  12421  mscl  12447  xmscl  12448  xmsge0  12449  xmseq0  12450  bj-peano4  12832