Theorem 3adant1 999

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

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

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

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

This theorem is referenced by:  3ad2ant2  1003  3ad2ant3  1004  rsp2e  2483  sbciegft  2939  reuhyp  4393  suc11g  4472  soinxp  4609  breldmg  4745  funopg  5157  funimaexglem  5206  fex2  5291  fnreseql  5530  ftpg  5604  mpoeq3ia  5836  mpofvex  6101  poxp  6129  smores3  6190  tfrlemibxssdm  6224  nndi  6382  nnmass  6383  nndir  6386  fnsnsplitdc  6401  nnaord  6405  nnaordr  6406  nnawordi  6411  nnmord  6413  ecopovtrn  6526  ecopovtrng  6529  ixpf  6614  mapxpen  6742  ltsopi  7128  addassnqg  7190  ltsonq  7206  ltmnqg  7209  distrnq0  7267  addlocpr  7344  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  ltpopr  7403  ltsopr  7404  addcanprg  7424  lttrsr  7570  ltsosr  7572  ltasrg  7578  recexgt0sr  7581  mulextsr1lem  7588  mulextsr1  7589  axpre-mulext  7696  adddir  7757  axltwlin  7832  axlttrn  7833  ltleletr  7846  letr  7847  mul32  7892  mul31  7893  add32  7921  subsub23  7967  addsubass  7972  subcan2  7987  subsub2  7990  nppcan2  7993  sub32  7996  nnncan  7997  nnncan2  7999  pnpcan2  8002  subdi  8147  subdir  8148  reapcotr  8360  receuap  8430  divmulap3  8437  divrecap  8448  divrecap2  8449  divsubdirap  8468  divdivap1  8483  redivclap  8491  div2negap  8495  ltmul2  8614  lemul2  8615  lemul2a  8617  lediv1  8627  gt0div  8628  ge0div  8629  ltdivmul  8634  ltdivmul2  8636  ledivmul2  8638  uzind2  9163  nn0ind  9165  fnn0ind  9167  uz3m2nn  9368  xrletr  9591  xrre2  9604  xleadd2a  9657  xleadd1  9658  xltadd2  9660  ixxdisj  9686  iooneg  9771  iccneg  9772  icoshft  9773  icoshftf1o  9774  icodisj  9775  fzen  9823  fzrev3  9867  2ffzeq  9918  fzoaddel2  9970  elfzodifsumelfzo  9978  ssfzo12bi  10002  fzoshftral  10015  adddivflid  10065  fldiv4p1lem1div2  10078  modqmulnn  10115  modqeqmodmin  10167  frec2uzf1od  10179  expdivap  10344  shftval2  10598  mulreap  10636  absdivap  10842  absdiflt  10864  absdifle  10865  abs3dif  10877  cau3  10887  ltmininf  11006  xrmaxlesup  11028  xrltmininf  11039  xrlemininf  11040  xrminltinf  11041  geoisum1c  11289  dvdsmulc  11521  dvdsmultr1  11531  dvdsmultr2  11533  dvdssub2  11535  oexpneg  11574  divalgb  11622  ndvdsadd  11628  gcdaddm  11672  modgcd  11679  dvdsgcd  11700  dvdsgcdb  11701  gcdass  11703  mulgcd  11704  absmulgcd  11705  rpmulgcd  11714  nn0seqcvgd  11722  algcvga  11732  lcmdvds  11760  lcmdvdsb  11765  lcmass  11766  coprmdvds  11773  coprmdvds2  11774  rpmul  11779  cncongr1  11784  cncongr2  11785  prmgt1  11812  qnumdenbi  11870  setsvala  11990  setsex  11991  unopn  12172  clsss  12287  opnssneib  12325  restabs  12344  upxp  12441  blpnfctr  12608  mscl  12634  xmscl  12635  xmsge0  12636  xmseq0  12637  bj-peano4  13153