Theorem 3adant1 1017

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

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

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 982

This theorem is referenced by:  3ad2ant2  1021  3ad2ant3  1022  rsp2e  2545  sbciegft  3016  reuhyp  4503  suc11g  4589  soinxp  4729  breldmg  4868  funopg  5288  funimaexglem  5337  fex2  5422  fnreseql  5668  ftpg  5742  mpoeq3ia  5983  funexw  6164  mpofvex  6256  poxp  6285  smores3  6346  tfrlemibxssdm  6380  nndi  6539  nnmass  6540  nndir  6543  fnsnsplitdc  6558  nnaord  6562  nnaordr  6563  nnawordi  6568  nnmord  6570  ecopovtrn  6686  ecopovtrng  6689  ixpf  6774  mapxpen  6904  netap  7314  2omotaplemap  7317  ltsopi  7380  addassnqg  7442  ltsonq  7458  ltmnqg  7461  distrnq0  7519  addlocpr  7596  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  ltpopr  7655  ltsopr  7656  addcanprg  7676  lttrsr  7822  ltsosr  7824  ltasrg  7830  recexgt0sr  7833  mulextsr1lem  7840  mulextsr1  7841  axpre-mulext  7948  adddir  8010  axltwlin  8087  axlttrn  8088  ltleletr  8101  letr  8102  mul32  8149  mul31  8150  add32  8178  subsub23  8224  addsubass  8229  subcan2  8244  subsub2  8247  nppcan2  8250  sub32  8253  nnncan  8254  nnncan2  8256  pnpcan2  8259  subdi  8404  subdir  8405  reapcotr  8617  receuap  8688  divmulap3  8696  divrecap  8707  divrecap2  8708  divsubdirap  8727  divdivap1  8742  redivclap  8750  div2negap  8754  ltmul2  8875  lemul2  8876  lemul2a  8878  lediv1  8888  gt0div  8889  ge0div  8890  ltdivmul  8895  ltdivmul2  8897  ledivmul2  8899  uzind2  9429  nn0ind  9431  fnn0ind  9433  uz3m2nn  9638  xrletr  9874  xrre2  9887  xleadd2a  9940  xleadd1  9941  xltadd2  9943  ixxdisj  9969  iooneg  10054  iccneg  10055  icoshft  10056  icoshftf1o  10057  icodisj  10058  fzen  10109  fzrev3  10153  2ffzeq  10207  fzoaddel2  10260  elfzodifsumelfzo  10268  ssfzo12bi  10292  fzoshftral  10305  adddivflid  10361  fldiv4p1lem1div2  10374  modqmulnn  10413  modqeqmodmin  10465  frec2uzf1od  10477  expdivap  10661  shftval2  10970  mulreap  11008  absdivap  11214  absdiflt  11236  absdifle  11237  abs3dif  11249  cau3  11259  ltmininf  11378  xrmaxlesup  11402  xrltmininf  11413  xrlemininf  11414  xrminltinf  11415  geoisum1c  11663  dvdsmulc  11962  dvdsmultr1  11974  dvdsmultr2  11976  dvdssub2  11978  oexpneg  12018  divalgb  12066  ndvdsadd  12072  gcdaddm  12121  modgcd  12128  dvdsgcd  12149  dvdsgcdb  12150  gcdass  12152  mulgcd  12153  absmulgcd  12154  rpmulgcd  12163  nn0seqcvgd  12179  algcvga  12189  lcmdvds  12217  lcmdvdsb  12222  lcmass  12223  coprmdvds  12230  coprmdvds2  12231  rpmul  12236  cncongr1  12241  cncongr2  12242  prmgt1  12270  qnumdenbi  12330  coprimeprodsq  12395  pythagtriplem4  12406  pythagtriplem8  12410  pythagtriplem9  12411  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pcpremul  12431  pcgcd  12467  setsvala  12649  setsex  12650  ressval2  12684  isgrpi  13096  grpsubrcan  13153  grpinvsub  13154  grpsubeq0  13158  grpsubadd0sub  13159  grpnpcan  13164  qussub  13307  ghmsub  13321  opprmulg  13567  rrgeq0  13761  lmodvsubval2  13838  rmodislmodlem  13846  rmodislmod  13847  lssintclm  13880  lssincl  13881  rnglidlmmgm  13992  cncrng  14057  unopn  14173  clsss  14286  opnssneib  14324  restabs  14343  upxp  14440  blpnfctr  14607  mscl  14633  xmscl  14634  xmsge0  14635  xmseq0  14636  rpdivcxp  15046  cxpcom  15071  rplogbreexp  15085  rplogbzexp  15086  rprelogbmulexp  15088  logbleb  15093  logblt  15094  lgsneg  15140  lgsne0  15154  lgsmodeq  15161  lgsmulsqcoprm  15162  gausslemma2dlem1a  15174  bj-peano4  15447