Theorem 3adant1 959

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  3ad2ant2  963  3ad2ant3  964  rsp2e  2422  sbciegft  2858  reuhyp  4268  suc11g  4346  soinxp  4476  breldmg  4610  funopg  5013  funimaexglem  5062  fex2  5143  fnreseql  5372  ftpg  5444  mpt2eq3ia  5671  mpt2fvex  5930  poxp  5954  smores3  6012  tfrlemibxssdm  6046  nndi  6201  nnmass  6202  nndir  6205  nnaord  6220  nnaordr  6221  nnawordi  6226  nnmord  6228  ecopovtrn  6341  ecopovtrng  6344  mapxpen  6516  ltsopi  6823  addassnqg  6885  ltsonq  6901  ltmnqg  6904  distrnq0  6962  addlocpr  7039  distrlem1prl  7085  distrlem1pru  7086  distrlem4prl  7087  distrlem4pru  7088  ltpopr  7098  ltsopr  7099  addcanprg  7119  lttrsr  7252  ltsosr  7254  ltasrg  7260  recexgt0sr  7263  mulextsr1lem  7269  mulextsr1  7270  axpre-mulext  7367  adddir  7423  axltwlin  7498  axlttrn  7499  ltleletr  7511  letr  7512  mul32  7556  mul31  7557  add32  7585  subsub23  7631  addsubass  7636  subcan2  7651  subsub2  7654  nppcan2  7657  sub32  7660  nnncan  7661  nnncan2  7663  pnpcan2  7666  subdi  7807  subdir  7808  reapcotr  8016  receuap  8077  divmulap3  8083  divrecap  8094  divrecap2  8095  divsubdirap  8114  divdivap1  8129  redivclap  8137  div2negap  8141  ltmul2  8252  lemul2  8253  lemul2a  8255  lediv1  8265  gt0div  8266  ge0div  8267  ltdivmul  8272  ltdivmul2  8274  ledivmul2  8276  uzind2  8791  nn0ind  8793  fnn0ind  8795  uz3m2nn  8993  xrletr  9205  xrre2  9215  ixxdisj  9253  iooneg  9337  iccneg  9338  icoshft  9339  icoshftf1o  9340  icodisj  9341  fzen  9389  fzrev3  9431  2ffzeq  9480  fzoaddel2  9532  elfzodifsumelfzo  9540  ssfzo12bi  9564  fzoshftral  9577  adddivflid  9627  fldiv4p1lem1div2  9640  modqmulnn  9677  modqeqmodmin  9729  frec2uzf1od  9741  expdivap  9905  shftval2  10157  mulreap  10194  absdivap  10399  absdiflt  10421  absdifle  10422  abs3dif  10434  cau3  10444  ltmininf  10560  dvdsmulc  10706  dvdsmultr1  10716  dvdsmultr2  10718  dvdssub2  10720  oexpneg  10759  divalgb  10807  ndvdsadd  10813  gcdaddm  10857  modgcd  10864  dvdsgcd  10883  dvdsgcdb  10884  gcdass  10886  mulgcd  10887  absmulgcd  10888  rpmulgcd  10897  nn0seqcvgd  10905  ialgcvga  10915  lcmdvds  10943  lcmdvdsb  10948  lcmass  10949  coprmdvds  10956  coprmdvds2  10957  rpmul  10962  cncongr1  10967  cncongr2  10968  prmgt1  10995  qnumdenbi  11052  bj-peano4  11295