Theorem 3adant1 1046

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant2  1050  3ad2ant3  1051  rsp2e  2601  sbciegft  3082  reuhyp  4618  suc11g  4704  soinxp  4845  breldmg  4987  funopg  5411  funimaexglem  5464  fex2  5556  fnreseql  5819  ftpg  5899  mpoeq3ia  6153  funexw  6341  mpofvex  6441  poxp  6468  suppval1  6479  smores3  6564  tfrlemibxssdm  6598  nndi  6759  nnmass  6760  nndir  6763  fnsnsplitdc  6778  nnaord  6782  nnaordr  6783  nnawordi  6788  nnmord  6790  ecopovtrn  6906  ecopovtrng  6909  ixpf  7002  f1oen4g  7038  f1dom4g  7039  mapxpen  7148  funisfsupp  7291  netap  7621  2omotaplemap  7624  ltsopi  7688  addassnqg  7750  ltsonq  7766  ltmnqg  7769  distrnq0  7827  addlocpr  7904  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  ltpopr  7963  ltsopr  7964  addcanprg  7984  lttrsr  8130  ltsosr  8132  ltasrg  8138  recexgt0sr  8141  mulextsr1lem  8148  mulextsr1  8149  axpre-mulext  8256  adddir  8318  axltwlin  8394  axlttrn  8395  ltleletr  8408  letr  8409  mul32  8458  mul31  8459  add32  8487  subsub23  8533  addsubass  8538  subcan2  8553  subsub2  8556  nppcan2  8559  sub32  8562  nnncan  8563  nnncan2  8565  pnpcan2  8568  subdi  8714  subdir  8715  reapcotr  8929  receuap  9002  divmulap3  9010  divrecap  9021  divrecap2  9022  divsubdirap  9041  divdivap1  9056  redivclap  9064  div2negap  9068  ltmul2  9189  lemul2  9190  lemul2a  9192  lediv1  9202  gt0div  9203  ge0div  9204  ltdivmul  9209  ltdivmul2  9211  ledivmul2  9213  uzind2  9763  nn0ind  9765  fnn0ind  9767  uz3m2nn  9983  xrletr  10221  xrre2  10234  xleadd2a  10287  xleadd1  10288  xltadd2  10290  ixxdisj  10316  iooneg  10401  iccneg  10402  icoshft  10403  icoshftf1o  10404  icodisj  10405  fzen  10458  fzrev3  10505  2ffzeq  10559  fzoaddel2  10619  elfzodifsumelfzo  10630  ssfzo12bi  10654  fzoshftral  10668  adddivflid  10742  fldiv4p1lem1div2  10755  modqmulnn  10794  modqeqmodmin  10846  frec2uzf1od  10858  expdivap  11042  ccatval1  11381  ccatass  11392  fzowrddc  11435  swrdval  11436  swrdnd  11447  swrd0g  11448  swrdfv2  11451  pfxsuff1eqwrdeq  11487  swrdswrdlem  11492  pfxccatin12lem2a  11515  pfxccatin12lem1  11516  shftval2  11607  mulreap  11645  absdivap  11852  absdiflt  11875  absdifle  11876  abs3dif  11888  cau3  11898  ltmininf  12019  xrmaxlesup  12044  xrltmininf  12055  xrlemininf  12056  xrminltinf  12057  geoisum1c  12306  dvdsmulc  12605  dvdsmultr1  12617  dvdsmultr2  12619  dvdssub2  12621  oexpneg  12663  divalgb  12711  ndvdsadd  12717  gcdaddm  12780  modgcd  12787  dvdsgcd  12808  dvdsgcdb  12809  gcdass  12811  mulgcd  12812  absmulgcd  12813  rpmulgcd  12822  nn0seqcvgd  12838  algcvga  12848  lcmdvds  12876  lcmdvdsb  12881  lcmass  12882  coprmdvds  12889  coprmdvds2  12890  rpmul  12895  cncongr1  12900  cncongr2  12901  prmgt1  12930  qnumdenbi  12991  coprimeprodsq  13059  pythagtriplem4  13070  pythagtriplem8  13074  pythagtriplem9  13075  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  pcpremul  13095  pcgcd  13131  setsvala  13435  setsex  13436  ressval2  13473  isgrpi  13882  grpsubrcan  13939  grpinvsub  13940  grpsubeq0  13944  grpsubadd0sub  13945  grpnpcan  13950  qussub  14093  ghmsub  14107  opprmulg  14460  rrgeq0  14657  lmodvsubval2  14763  rmodislmodlem  14771  rmodislmod  14772  lssintclm  14805  lssincl  14806  rnglidlmmgm  14917  cncrng  14990  unopn  15197  clsss  15310  opnssneib  15348  restabs  15367  upxp  15464  blpnfctr  15631  mscl  15657  xmscl  15658  xmsge0  15659  xmseq0  15660  mpomulcn  15758  rpdivcxp  16108  cxpcom  16135  rplogbreexp  16150  rplogbzexp  16151  rprelogbmulexp  16153  logbleb  16158  logblt  16159  lgsneg  16309  lgsne0  16323  lgsmodeq  16330  lgsmulsqcoprm  16331  gausslemma2dlem1a  16343  funvtxdm2domval  16436  funiedgdm2domval  16437  iedgedgg  16468  iswlk  16730  uspgr2wlkeq  16772  uspgr2wlkeq2  16773  uspgr2wlkeqi  16774  istrl  16792  clwwlkgt0  16803  iseupth  16854  bj-peano4  17147