Theorem 3adant1 1000

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

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

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 965

This theorem is referenced by:  3ad2ant2  1004  3ad2ant3  1005  rsp2e  2505  sbciegft  2963  reuhyp  4426  suc11g  4510  soinxp  4649  breldmg  4785  funopg  5197  funimaexglem  5246  fex2  5331  fnreseql  5570  ftpg  5644  mpoeq3ia  5876  mpofvex  6141  poxp  6169  smores3  6230  tfrlemibxssdm  6264  nndi  6422  nnmass  6423  nndir  6426  fnsnsplitdc  6441  nnaord  6445  nnaordr  6446  nnawordi  6451  nnmord  6453  ecopovtrn  6566  ecopovtrng  6569  ixpf  6654  mapxpen  6782  ltsopi  7219  addassnqg  7281  ltsonq  7297  ltmnqg  7300  distrnq0  7358  addlocpr  7435  distrlem1prl  7481  distrlem1pru  7482  distrlem4prl  7483  distrlem4pru  7484  ltpopr  7494  ltsopr  7495  addcanprg  7515  lttrsr  7661  ltsosr  7663  ltasrg  7669  recexgt0sr  7672  mulextsr1lem  7679  mulextsr1  7680  axpre-mulext  7787  adddir  7848  axltwlin  7924  axlttrn  7925  ltleletr  7938  letr  7939  mul32  7984  mul31  7985  add32  8013  subsub23  8059  addsubass  8064  subcan2  8079  subsub2  8082  nppcan2  8085  sub32  8088  nnncan  8089  nnncan2  8091  pnpcan2  8094  subdi  8239  subdir  8240  reapcotr  8452  receuap  8522  divmulap3  8529  divrecap  8540  divrecap2  8541  divsubdirap  8560  divdivap1  8575  redivclap  8583  div2negap  8587  ltmul2  8706  lemul2  8707  lemul2a  8709  lediv1  8719  gt0div  8720  ge0div  8721  ltdivmul  8726  ltdivmul2  8728  ledivmul2  8730  uzind2  9255  nn0ind  9257  fnn0ind  9259  uz3m2nn  9463  xrletr  9690  xrre2  9703  xleadd2a  9756  xleadd1  9757  xltadd2  9759  ixxdisj  9785  iooneg  9870  iccneg  9871  icoshft  9872  icoshftf1o  9873  icodisj  9874  fzen  9923  fzrev3  9967  2ffzeq  10018  fzoaddel2  10070  elfzodifsumelfzo  10078  ssfzo12bi  10102  fzoshftral  10115  adddivflid  10169  fldiv4p1lem1div2  10182  modqmulnn  10219  modqeqmodmin  10271  frec2uzf1od  10283  expdivap  10448  shftval2  10703  mulreap  10741  absdivap  10947  absdiflt  10969  absdifle  10970  abs3dif  10982  cau3  10992  ltmininf  11111  xrmaxlesup  11133  xrltmininf  11144  xrlemininf  11145  xrminltinf  11146  geoisum1c  11394  dvdsmulc  11688  dvdsmultr1  11698  dvdsmultr2  11700  dvdssub2  11702  oexpneg  11741  divalgb  11789  ndvdsadd  11795  gcdaddm  11840  modgcd  11847  dvdsgcd  11868  dvdsgcdb  11869  gcdass  11871  mulgcd  11872  absmulgcd  11873  rpmulgcd  11882  nn0seqcvgd  11890  algcvga  11900  lcmdvds  11928  lcmdvdsb  11933  lcmass  11934  coprmdvds  11941  coprmdvds2  11942  rpmul  11947  cncongr1  11952  cncongr2  11953  prmgt1  11980  qnumdenbi  12038  setsvala  12168  setsex  12169  unopn  12350  clsss  12465  opnssneib  12503  restabs  12522  upxp  12619  blpnfctr  12786  mscl  12812  xmscl  12813  xmsge0  12814  xmseq0  12815  rpdivcxp  13179  cxpcom  13204  rplogbreexp  13217  rplogbzexp  13218  rprelogbmulexp  13220  logbleb  13225  logblt  13226  bj-peano4  13476