Theorem 3adant1 1015

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

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

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 980

This theorem is referenced by:  3ad2ant2  1019  3ad2ant3  1020  rsp2e  2528  sbciegft  2995  reuhyp  4474  suc11g  4558  soinxp  4698  breldmg  4835  funopg  5252  funimaexglem  5301  fex2  5386  fnreseql  5628  ftpg  5702  mpoeq3ia  5942  funexw  6115  mpofvex  6206  poxp  6235  smores3  6296  tfrlemibxssdm  6330  nndi  6489  nnmass  6490  nndir  6493  fnsnsplitdc  6508  nnaord  6512  nnaordr  6513  nnawordi  6518  nnmord  6520  ecopovtrn  6634  ecopovtrng  6637  ixpf  6722  mapxpen  6850  netap  7255  2omotaplemap  7258  ltsopi  7321  addassnqg  7383  ltsonq  7399  ltmnqg  7402  distrnq0  7460  addlocpr  7537  distrlem1prl  7583  distrlem1pru  7584  distrlem4prl  7585  distrlem4pru  7586  ltpopr  7596  ltsopr  7597  addcanprg  7617  lttrsr  7763  ltsosr  7765  ltasrg  7771  recexgt0sr  7774  mulextsr1lem  7781  mulextsr1  7782  axpre-mulext  7889  adddir  7950  axltwlin  8027  axlttrn  8028  ltleletr  8041  letr  8042  mul32  8089  mul31  8090  add32  8118  subsub23  8164  addsubass  8169  subcan2  8184  subsub2  8187  nppcan2  8190  sub32  8193  nnncan  8194  nnncan2  8196  pnpcan2  8199  subdi  8344  subdir  8345  reapcotr  8557  receuap  8628  divmulap3  8636  divrecap  8647  divrecap2  8648  divsubdirap  8667  divdivap1  8682  redivclap  8690  div2negap  8694  ltmul2  8815  lemul2  8816  lemul2a  8818  lediv1  8828  gt0div  8829  ge0div  8830  ltdivmul  8835  ltdivmul2  8837  ledivmul2  8839  uzind2  9367  nn0ind  9369  fnn0ind  9371  uz3m2nn  9575  xrletr  9810  xrre2  9823  xleadd2a  9876  xleadd1  9877  xltadd2  9879  ixxdisj  9905  iooneg  9990  iccneg  9991  icoshft  9992  icoshftf1o  9993  icodisj  9994  fzen  10045  fzrev3  10089  2ffzeq  10143  fzoaddel2  10195  elfzodifsumelfzo  10203  ssfzo12bi  10227  fzoshftral  10240  adddivflid  10294  fldiv4p1lem1div2  10307  modqmulnn  10344  modqeqmodmin  10396  frec2uzf1od  10408  expdivap  10573  shftval2  10837  mulreap  10875  absdivap  11081  absdiflt  11103  absdifle  11104  abs3dif  11116  cau3  11126  ltmininf  11245  xrmaxlesup  11269  xrltmininf  11280  xrlemininf  11281  xrminltinf  11282  geoisum1c  11530  dvdsmulc  11828  dvdsmultr1  11840  dvdsmultr2  11842  dvdssub2  11844  oexpneg  11884  divalgb  11932  ndvdsadd  11938  gcdaddm  11987  modgcd  11994  dvdsgcd  12015  dvdsgcdb  12016  gcdass  12018  mulgcd  12019  absmulgcd  12020  rpmulgcd  12029  nn0seqcvgd  12043  algcvga  12053  lcmdvds  12081  lcmdvdsb  12086  lcmass  12087  coprmdvds  12094  coprmdvds2  12095  rpmul  12100  cncongr1  12105  cncongr2  12106  prmgt1  12134  qnumdenbi  12194  coprimeprodsq  12259  pythagtriplem4  12270  pythagtriplem8  12274  pythagtriplem9  12275  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  pcpremul  12295  pcgcd  12330  setsvala  12495  setsex  12496  ressval2  12528  isgrpi  12905  grpsubrcan  12956  grpinvsub  12957  grpsubeq0  12961  grpsubadd0sub  12962  grpnpcan  12967  opprmulg  13248  lmodvsubval2  13437  rmodislmodlem  13445  rmodislmod  13446  lssintclm  13476  lssincl  13477  cncrng  13548  unopn  13590  clsss  13703  opnssneib  13741  restabs  13760  upxp  13857  blpnfctr  14024  mscl  14050  xmscl  14051  xmsge0  14052  xmseq0  14053  rpdivcxp  14417  cxpcom  14442  rplogbreexp  14456  rplogbzexp  14457  rprelogbmulexp  14459  logbleb  14464  logblt  14465  lgsneg  14510  lgsne0  14524  lgsmodeq  14531  lgsmulsqcoprm  14532  bj-peano4  14792