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  2993  reuhyp  4468  suc11g  4552  soinxp  4692  breldmg  4828  funopg  5245  funimaexglem  5294  fex2  5379  fnreseql  5621  ftpg  5695  mpoeq3ia  5933  funexw  6106  mpofvex  6197  poxp  6226  smores3  6287  tfrlemibxssdm  6321  nndi  6480  nnmass  6481  nndir  6484  fnsnsplitdc  6499  nnaord  6503  nnaordr  6504  nnawordi  6509  nnmord  6511  ecopovtrn  6625  ecopovtrng  6628  ixpf  6713  mapxpen  6841  ltsopi  7297  addassnqg  7359  ltsonq  7375  ltmnqg  7378  distrnq0  7436  addlocpr  7513  distrlem1prl  7559  distrlem1pru  7560  distrlem4prl  7561  distrlem4pru  7562  ltpopr  7572  ltsopr  7573  addcanprg  7593  lttrsr  7739  ltsosr  7741  ltasrg  7747  recexgt0sr  7750  mulextsr1lem  7757  mulextsr1  7758  axpre-mulext  7865  adddir  7926  axltwlin  8002  axlttrn  8003  ltleletr  8016  letr  8017  mul32  8064  mul31  8065  add32  8093  subsub23  8139  addsubass  8144  subcan2  8159  subsub2  8162  nppcan2  8165  sub32  8168  nnncan  8169  nnncan2  8171  pnpcan2  8174  subdi  8319  subdir  8320  reapcotr  8532  receuap  8602  divmulap3  8610  divrecap  8621  divrecap2  8622  divsubdirap  8641  divdivap1  8656  redivclap  8664  div2negap  8668  ltmul2  8789  lemul2  8790  lemul2a  8792  lediv1  8802  gt0div  8803  ge0div  8804  ltdivmul  8809  ltdivmul2  8811  ledivmul2  8813  uzind2  9341  nn0ind  9343  fnn0ind  9345  uz3m2nn  9549  xrletr  9782  xrre2  9795  xleadd2a  9848  xleadd1  9849  xltadd2  9851  ixxdisj  9877  iooneg  9962  iccneg  9963  icoshft  9964  icoshftf1o  9965  icodisj  9966  fzen  10016  fzrev3  10060  2ffzeq  10114  fzoaddel2  10166  elfzodifsumelfzo  10174  ssfzo12bi  10198  fzoshftral  10211  adddivflid  10265  fldiv4p1lem1div2  10278  modqmulnn  10315  modqeqmodmin  10367  frec2uzf1od  10379  expdivap  10544  shftval2  10806  mulreap  10844  absdivap  11050  absdiflt  11072  absdifle  11073  abs3dif  11085  cau3  11095  ltmininf  11214  xrmaxlesup  11238  xrltmininf  11249  xrlemininf  11250  xrminltinf  11251  geoisum1c  11499  dvdsmulc  11797  dvdsmultr1  11809  dvdsmultr2  11811  dvdssub2  11813  oexpneg  11852  divalgb  11900  ndvdsadd  11906  gcdaddm  11955  modgcd  11962  dvdsgcd  11983  dvdsgcdb  11984  gcdass  11986  mulgcd  11987  absmulgcd  11988  rpmulgcd  11997  nn0seqcvgd  12011  algcvga  12021  lcmdvds  12049  lcmdvdsb  12054  lcmass  12055  coprmdvds  12062  coprmdvds2  12063  rpmul  12068  cncongr1  12073  cncongr2  12074  prmgt1  12102  qnumdenbi  12162  coprimeprodsq  12227  pythagtriplem4  12238  pythagtriplem8  12242  pythagtriplem9  12243  pythagtriplem12  12245  pythagtriplem14  12247  pythagtriplem16  12249  pcpremul  12263  pcgcd  12298  setsvala  12463  setsex  12464  ressval2  12495  isgrpi  12777  grpsubrcan  12827  grpinvsub  12828  grpsubeq0  12832  grpsubadd0sub  12833  grpnpcan  12838  opprmulg  13055  unopn  13136  clsss  13251  opnssneib  13289  restabs  13308  upxp  13405  blpnfctr  13572  mscl  13598  xmscl  13599  xmsge0  13600  xmseq0  13601  rpdivcxp  13965  cxpcom  13990  rplogbreexp  14004  rplogbzexp  14005  rprelogbmulexp  14007  logbleb  14012  logblt  14013  lgsneg  14058  lgsne0  14072  lgsmodeq  14079  lgsmulsqcoprm  14080  bj-peano4  14329