Theorem 3adant1 1018

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

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

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 983

This theorem is referenced by:  3ad2ant2  1022  3ad2ant3  1023  rsp2e  2558  sbciegft  3033  reuhyp  4526  suc11g  4612  soinxp  4752  breldmg  4892  funopg  5313  funimaexglem  5365  fex2  5453  fnreseql  5702  ftpg  5780  mpoeq3ia  6022  funexw  6209  mpofvex  6303  poxp  6330  smores3  6391  tfrlemibxssdm  6425  nndi  6584  nnmass  6585  nndir  6588  fnsnsplitdc  6603  nnaord  6607  nnaordr  6608  nnawordi  6613  nnmord  6615  ecopovtrn  6731  ecopovtrng  6734  ixpf  6819  f1oen4g  6855  f1dom4g  6856  mapxpen  6959  netap  7381  2omotaplemap  7384  ltsopi  7448  addassnqg  7510  ltsonq  7526  ltmnqg  7529  distrnq0  7587  addlocpr  7664  distrlem1prl  7710  distrlem1pru  7711  distrlem4prl  7712  distrlem4pru  7713  ltpopr  7723  ltsopr  7724  addcanprg  7744  lttrsr  7890  ltsosr  7892  ltasrg  7898  recexgt0sr  7901  mulextsr1lem  7908  mulextsr1  7909  axpre-mulext  8016  adddir  8078  axltwlin  8155  axlttrn  8156  ltleletr  8169  letr  8170  mul32  8217  mul31  8218  add32  8246  subsub23  8292  addsubass  8297  subcan2  8312  subsub2  8315  nppcan2  8318  sub32  8321  nnncan  8322  nnncan2  8324  pnpcan2  8327  subdi  8472  subdir  8473  reapcotr  8686  receuap  8757  divmulap3  8765  divrecap  8776  divrecap2  8777  divsubdirap  8796  divdivap1  8811  redivclap  8819  div2negap  8823  ltmul2  8944  lemul2  8945  lemul2a  8947  lediv1  8957  gt0div  8958  ge0div  8959  ltdivmul  8964  ltdivmul2  8966  ledivmul2  8968  uzind2  9500  nn0ind  9502  fnn0ind  9504  uz3m2nn  9709  xrletr  9945  xrre2  9958  xleadd2a  10011  xleadd1  10012  xltadd2  10014  ixxdisj  10040  iooneg  10125  iccneg  10126  icoshft  10127  icoshftf1o  10128  icodisj  10129  fzen  10180  fzrev3  10224  2ffzeq  10278  fzoaddel2  10336  elfzodifsumelfzo  10347  ssfzo12bi  10371  fzoshftral  10384  adddivflid  10452  fldiv4p1lem1div2  10465  modqmulnn  10504  modqeqmodmin  10556  frec2uzf1od  10568  expdivap  10752  ccatval1  11071  ccatass  11082  fzowrddc  11118  swrdval  11119  swrdnd  11130  swrd0g  11131  swrdfv2  11134  pfxsuff1eqwrdeq  11170  swrdswrdlem  11175  shftval2  11207  mulreap  11245  absdivap  11451  absdiflt  11473  absdifle  11474  abs3dif  11486  cau3  11496  ltmininf  11616  xrmaxlesup  11640  xrltmininf  11651  xrlemininf  11652  xrminltinf  11653  geoisum1c  11901  dvdsmulc  12200  dvdsmultr1  12212  dvdsmultr2  12214  dvdssub2  12216  oexpneg  12258  divalgb  12306  ndvdsadd  12312  gcdaddm  12375  modgcd  12382  dvdsgcd  12403  dvdsgcdb  12404  gcdass  12406  mulgcd  12407  absmulgcd  12408  rpmulgcd  12417  nn0seqcvgd  12433  algcvga  12443  lcmdvds  12471  lcmdvdsb  12476  lcmass  12477  coprmdvds  12484  coprmdvds2  12485  rpmul  12490  cncongr1  12495  cncongr2  12496  prmgt1  12524  qnumdenbi  12584  coprimeprodsq  12650  pythagtriplem4  12661  pythagtriplem8  12665  pythagtriplem9  12666  pythagtriplem12  12668  pythagtriplem14  12670  pythagtriplem16  12672  pcpremul  12686  pcgcd  12722  setsvala  12933  setsex  12934  ressval2  12968  isgrpi  13426  grpsubrcan  13483  grpinvsub  13484  grpsubeq0  13488  grpsubadd0sub  13489  grpnpcan  13494  qussub  13643  ghmsub  13657  opprmulg  13903  rrgeq0  14097  lmodvsubval2  14174  rmodislmodlem  14182  rmodislmod  14183  lssintclm  14216  lssincl  14217  rnglidlmmgm  14328  cncrng  14401  unopn  14547  clsss  14660  opnssneib  14698  restabs  14717  upxp  14814  blpnfctr  14981  mscl  15007  xmscl  15008  xmsge0  15009  xmseq0  15010  mpomulcn  15108  rpdivcxp  15453  cxpcom  15480  rplogbreexp  15495  rplogbzexp  15496  rprelogbmulexp  15498  logbleb  15503  logblt  15504  lgsneg  15571  lgsne0  15585  lgsmodeq  15592  lgsmulsqcoprm  15593  gausslemma2dlem1a  15605  funvtxdm2domval  15698  funiedgdm2domval  15699  iedgedgg  15727  bj-peano4  16025