Theorem 3adant1 1042

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

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

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 1007

This theorem is referenced by:  3ad2ant2  1046  3ad2ant3  1047  rsp2e  2595  sbciegft  3076  reuhyp  4598  suc11g  4684  soinxp  4825  breldmg  4967  funopg  5391  funimaexglem  5444  fex2  5536  fnreseql  5793  ftpg  5873  mpoeq3ia  6126  funexw  6314  mpofvex  6414  poxp  6441  suppval1  6452  smores3  6537  tfrlemibxssdm  6571  nndi  6732  nnmass  6733  nndir  6736  fnsnsplitdc  6751  nnaord  6755  nnaordr  6756  nnawordi  6761  nnmord  6763  ecopovtrn  6879  ecopovtrng  6882  ixpf  6968  f1oen4g  7004  f1dom4g  7005  mapxpen  7114  funisfsupp  7257  netap  7584  2omotaplemap  7587  ltsopi  7651  addassnqg  7713  ltsonq  7729  ltmnqg  7732  distrnq0  7790  addlocpr  7867  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  ltpopr  7926  ltsopr  7927  addcanprg  7947  lttrsr  8093  ltsosr  8095  ltasrg  8101  recexgt0sr  8104  mulextsr1lem  8111  mulextsr1  8112  axpre-mulext  8219  adddir  8281  axltwlin  8357  axlttrn  8358  ltleletr  8371  letr  8372  mul32  8419  mul31  8420  add32  8448  subsub23  8494  addsubass  8499  subcan2  8514  subsub2  8517  nppcan2  8520  sub32  8523  nnncan  8524  nnncan2  8526  pnpcan2  8529  subdi  8675  subdir  8676  reapcotr  8889  receuap  8960  divmulap3  8968  divrecap  8979  divrecap2  8980  divsubdirap  8999  divdivap1  9014  redivclap  9022  div2negap  9026  ltmul2  9147  lemul2  9148  lemul2a  9150  lediv1  9160  gt0div  9161  ge0div  9162  ltdivmul  9167  ltdivmul2  9169  ledivmul2  9171  uzind2  9708  nn0ind  9710  fnn0ind  9712  uz3m2nn  9923  xrletr  10160  xrre2  10173  xleadd2a  10226  xleadd1  10227  xltadd2  10229  ixxdisj  10255  iooneg  10340  iccneg  10341  icoshft  10342  icoshftf1o  10343  icodisj  10344  fzen  10397  fzrev3  10443  2ffzeq  10497  fzoaddel2  10557  elfzodifsumelfzo  10568  ssfzo12bi  10592  fzoshftral  10606  adddivflid  10676  fldiv4p1lem1div2  10689  modqmulnn  10728  modqeqmodmin  10780  frec2uzf1od  10792  expdivap  10976  ccatval1  11310  ccatass  11321  fzowrddc  11364  swrdval  11365  swrdnd  11376  swrd0g  11377  swrdfv2  11380  pfxsuff1eqwrdeq  11416  swrdswrdlem  11421  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  shftval2  11536  mulreap  11574  absdivap  11780  absdiflt  11802  absdifle  11803  abs3dif  11815  cau3  11825  ltmininf  11945  xrmaxlesup  11969  xrltmininf  11980  xrlemininf  11981  xrminltinf  11982  geoisum1c  12231  dvdsmulc  12530  dvdsmultr1  12542  dvdsmultr2  12544  dvdssub2  12546  oexpneg  12588  divalgb  12636  ndvdsadd  12642  gcdaddm  12705  modgcd  12712  dvdsgcd  12733  dvdsgcdb  12734  gcdass  12736  mulgcd  12737  absmulgcd  12738  rpmulgcd  12747  nn0seqcvgd  12763  algcvga  12773  lcmdvds  12801  lcmdvdsb  12806  lcmass  12807  coprmdvds  12814  coprmdvds2  12815  rpmul  12820  cncongr1  12825  cncongr2  12826  prmgt1  12854  qnumdenbi  12914  coprimeprodsq  12980  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pcpremul  13016  pcgcd  13052  setsvala  13327  setsex  13328  ressval2  13363  isgrpi  13779  grpsubrcan  13836  grpinvsub  13837  grpsubeq0  13841  grpsubadd0sub  13842  grpnpcan  13847  qussub  13990  ghmsub  14004  opprmulg  14314  rrgeq0  14511  lmodvsubval2  14616  rmodislmodlem  14624  rmodislmod  14625  lssintclm  14658  lssincl  14659  rnglidlmmgm  14770  cncrng  14843  unopn  14996  clsss  15109  opnssneib  15147  restabs  15166  upxp  15263  blpnfctr  15430  mscl  15456  xmscl  15457  xmsge0  15458  xmseq0  15459  mpomulcn  15557  rpdivcxp  15902  cxpcom  15929  rplogbreexp  15944  rplogbzexp  15945  rprelogbmulexp  15947  logbleb  15952  logblt  15953  lgsneg  16023  lgsne0  16037  lgsmodeq  16044  lgsmulsqcoprm  16045  gausslemma2dlem1a  16057  funvtxdm2domval  16150  funiedgdm2domval  16151  iedgedgg  16182  iswlk  16444  uspgr2wlkeq  16486  uspgr2wlkeq2  16487  uspgr2wlkeqi  16488  istrl  16506  clwwlkgt0  16517  iseupth  16568  bj-peano4  16851