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  2541  sbciegft  3008  reuhyp  4493  suc11g  4577  soinxp  4717  breldmg  4854  funopg  5272  funimaexglem  5321  fex2  5406  fnreseql  5650  ftpg  5724  mpoeq3ia  5965  funexw  6141  mpofvex  6232  poxp  6261  smores3  6322  tfrlemibxssdm  6356  nndi  6515  nnmass  6516  nndir  6519  fnsnsplitdc  6534  nnaord  6538  nnaordr  6539  nnawordi  6544  nnmord  6546  ecopovtrn  6662  ecopovtrng  6665  ixpf  6750  mapxpen  6880  netap  7288  2omotaplemap  7291  ltsopi  7354  addassnqg  7416  ltsonq  7432  ltmnqg  7435  distrnq0  7493  addlocpr  7570  distrlem1prl  7616  distrlem1pru  7617  distrlem4prl  7618  distrlem4pru  7619  ltpopr  7629  ltsopr  7630  addcanprg  7650  lttrsr  7796  ltsosr  7798  ltasrg  7804  recexgt0sr  7807  mulextsr1lem  7814  mulextsr1  7815  axpre-mulext  7922  adddir  7983  axltwlin  8060  axlttrn  8061  ltleletr  8074  letr  8075  mul32  8122  mul31  8123  add32  8151  subsub23  8197  addsubass  8202  subcan2  8217  subsub2  8220  nppcan2  8223  sub32  8226  nnncan  8227  nnncan2  8229  pnpcan2  8232  subdi  8377  subdir  8378  reapcotr  8590  receuap  8661  divmulap3  8669  divrecap  8680  divrecap2  8681  divsubdirap  8700  divdivap1  8715  redivclap  8723  div2negap  8727  ltmul2  8848  lemul2  8849  lemul2a  8851  lediv1  8861  gt0div  8862  ge0div  8863  ltdivmul  8868  ltdivmul2  8870  ledivmul2  8872  uzind2  9400  nn0ind  9402  fnn0ind  9404  uz3m2nn  9609  xrletr  9844  xrre2  9857  xleadd2a  9910  xleadd1  9911  xltadd2  9913  ixxdisj  9939  iooneg  10024  iccneg  10025  icoshft  10026  icoshftf1o  10027  icodisj  10028  fzen  10079  fzrev3  10123  2ffzeq  10177  fzoaddel2  10229  elfzodifsumelfzo  10237  ssfzo12bi  10261  fzoshftral  10274  adddivflid  10329  fldiv4p1lem1div2  10342  modqmulnn  10379  modqeqmodmin  10431  frec2uzf1od  10443  expdivap  10611  shftval2  10876  mulreap  10914  absdivap  11120  absdiflt  11142  absdifle  11143  abs3dif  11155  cau3  11165  ltmininf  11284  xrmaxlesup  11308  xrltmininf  11319  xrlemininf  11320  xrminltinf  11321  geoisum1c  11569  dvdsmulc  11867  dvdsmultr1  11879  dvdsmultr2  11881  dvdssub2  11883  oexpneg  11923  divalgb  11971  ndvdsadd  11977  gcdaddm  12026  modgcd  12033  dvdsgcd  12054  dvdsgcdb  12055  gcdass  12057  mulgcd  12058  absmulgcd  12059  rpmulgcd  12068  nn0seqcvgd  12084  algcvga  12094  lcmdvds  12122  lcmdvdsb  12127  lcmass  12128  coprmdvds  12135  coprmdvds2  12136  rpmul  12141  cncongr1  12146  cncongr2  12147  prmgt1  12175  qnumdenbi  12235  coprimeprodsq  12300  pythagtriplem4  12311  pythagtriplem8  12315  pythagtriplem9  12316  pythagtriplem12  12318  pythagtriplem14  12320  pythagtriplem16  12322  pcpremul  12336  pcgcd  12372  setsvala  12554  setsex  12555  ressval2  12589  isgrpi  12992  grpsubrcan  13048  grpinvsub  13049  grpsubeq0  13053  grpsubadd0sub  13054  grpnpcan  13059  qussub  13201  ghmsub  13215  opprmulg  13446  lmodvsubval2  13683  rmodislmodlem  13691  rmodislmod  13692  lssintclm  13725  lssincl  13726  rnglidlmmgm  13837  cncrng  13897  unopn  13990  clsss  14103  opnssneib  14141  restabs  14160  upxp  14257  blpnfctr  14424  mscl  14450  xmscl  14451  xmsge0  14452  xmseq0  14453  rpdivcxp  14817  cxpcom  14842  rplogbreexp  14856  rplogbzexp  14857  rprelogbmulexp  14859  logbleb  14864  logblt  14865  lgsneg  14911  lgsne0  14925  lgsmodeq  14932  lgsmulsqcoprm  14933  bj-peano4  15193