Theorem 3adant1 1039

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

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 1004

This theorem is referenced by:  3ad2ant2  1043  3ad2ant3  1044  rsp2e  2581  sbciegft  3059  reuhyp  4562  suc11g  4648  soinxp  4788  breldmg  4928  funopg  5351  funimaexglem  5403  fex2  5491  fnreseql  5744  ftpg  5822  mpoeq3ia  6068  funexw  6255  mpofvex  6349  poxp  6376  smores3  6437  tfrlemibxssdm  6471  nndi  6630  nnmass  6631  nndir  6634  fnsnsplitdc  6649  nnaord  6653  nnaordr  6654  nnawordi  6659  nnmord  6661  ecopovtrn  6777  ecopovtrng  6780  ixpf  6865  f1oen4g  6901  f1dom4g  6902  mapxpen  7005  netap  7436  2omotaplemap  7439  ltsopi  7503  addassnqg  7565  ltsonq  7581  ltmnqg  7584  distrnq0  7642  addlocpr  7719  distrlem1prl  7765  distrlem1pru  7766  distrlem4prl  7767  distrlem4pru  7768  ltpopr  7778  ltsopr  7779  addcanprg  7799  lttrsr  7945  ltsosr  7947  ltasrg  7953  recexgt0sr  7956  mulextsr1lem  7963  mulextsr1  7964  axpre-mulext  8071  adddir  8133  axltwlin  8210  axlttrn  8211  ltleletr  8224  letr  8225  mul32  8272  mul31  8273  add32  8301  subsub23  8347  addsubass  8352  subcan2  8367  subsub2  8370  nppcan2  8373  sub32  8376  nnncan  8377  nnncan2  8379  pnpcan2  8382  subdi  8527  subdir  8528  reapcotr  8741  receuap  8812  divmulap3  8820  divrecap  8831  divrecap2  8832  divsubdirap  8851  divdivap1  8866  redivclap  8874  div2negap  8878  ltmul2  8999  lemul2  9000  lemul2a  9002  lediv1  9012  gt0div  9013  ge0div  9014  ltdivmul  9019  ltdivmul2  9021  ledivmul2  9023  uzind2  9555  nn0ind  9557  fnn0ind  9559  uz3m2nn  9764  xrletr  10000  xrre2  10013  xleadd2a  10066  xleadd1  10067  xltadd2  10069  ixxdisj  10095  iooneg  10180  iccneg  10181  icoshft  10182  icoshftf1o  10183  icodisj  10184  fzen  10235  fzrev3  10279  2ffzeq  10333  fzoaddel2  10391  elfzodifsumelfzo  10402  ssfzo12bi  10426  fzoshftral  10439  adddivflid  10507  fldiv4p1lem1div2  10520  modqmulnn  10559  modqeqmodmin  10611  frec2uzf1od  10623  expdivap  10807  ccatval1  11127  ccatass  11138  fzowrddc  11174  swrdval  11175  swrdnd  11186  swrd0g  11187  swrdfv2  11190  pfxsuff1eqwrdeq  11226  swrdswrdlem  11231  pfxccatin12lem2a  11254  pfxccatin12lem1  11255  shftval2  11332  mulreap  11370  absdivap  11576  absdiflt  11598  absdifle  11599  abs3dif  11611  cau3  11621  ltmininf  11741  xrmaxlesup  11765  xrltmininf  11776  xrlemininf  11777  xrminltinf  11778  geoisum1c  12026  dvdsmulc  12325  dvdsmultr1  12337  dvdsmultr2  12339  dvdssub2  12341  oexpneg  12383  divalgb  12431  ndvdsadd  12437  gcdaddm  12500  modgcd  12507  dvdsgcd  12528  dvdsgcdb  12529  gcdass  12531  mulgcd  12532  absmulgcd  12533  rpmulgcd  12542  nn0seqcvgd  12558  algcvga  12568  lcmdvds  12596  lcmdvdsb  12601  lcmass  12602  coprmdvds  12609  coprmdvds2  12610  rpmul  12615  cncongr1  12620  cncongr2  12621  prmgt1  12649  qnumdenbi  12709  coprimeprodsq  12775  pythagtriplem4  12786  pythagtriplem8  12790  pythagtriplem9  12791  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pcpremul  12811  pcgcd  12847  setsvala  13058  setsex  13059  ressval2  13094  isgrpi  13552  grpsubrcan  13609  grpinvsub  13610  grpsubeq0  13614  grpsubadd0sub  13615  grpnpcan  13620  qussub  13769  ghmsub  13783  opprmulg  14029  rrgeq0  14223  lmodvsubval2  14300  rmodislmodlem  14308  rmodislmod  14309  lssintclm  14342  lssincl  14343  rnglidlmmgm  14454  cncrng  14527  unopn  14673  clsss  14786  opnssneib  14824  restabs  14843  upxp  14940  blpnfctr  15107  mscl  15133  xmscl  15134  xmsge0  15135  xmseq0  15136  mpomulcn  15234  rpdivcxp  15579  cxpcom  15606  rplogbreexp  15621  rplogbzexp  15622  rprelogbmulexp  15624  logbleb  15629  logblt  15630  lgsneg  15697  lgsne0  15711  lgsmodeq  15718  lgsmulsqcoprm  15719  gausslemma2dlem1a  15731  funvtxdm2domval  15824  funiedgdm2domval  15825  iedgedgg  15855  iswlk  16029  bj-peano4  16276