Theorem 3adant1 1039

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

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

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 1004

This theorem is referenced by:  3ad2ant2  1043  3ad2ant3  1044  rsp2e  2581  sbciegft  3060  reuhyp  4567  suc11g  4653  soinxp  4794  breldmg  4935  funopg  5358  funimaexglem  5410  fex2  5500  fnreseql  5753  ftpg  5833  mpoeq3ia  6081  funexw  6269  mpofvex  6365  poxp  6392  smores3  6454  tfrlemibxssdm  6488  nndi  6649  nnmass  6650  nndir  6653  fnsnsplitdc  6668  nnaord  6672  nnaordr  6673  nnawordi  6678  nnmord  6680  ecopovtrn  6796  ecopovtrng  6799  ixpf  6884  f1oen4g  6920  f1dom4g  6921  mapxpen  7029  netap  7463  2omotaplemap  7466  ltsopi  7530  addassnqg  7592  ltsonq  7608  ltmnqg  7611  distrnq0  7669  addlocpr  7746  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  ltpopr  7805  ltsopr  7806  addcanprg  7826  lttrsr  7972  ltsosr  7974  ltasrg  7980  recexgt0sr  7983  mulextsr1lem  7990  mulextsr1  7991  axpre-mulext  8098  adddir  8160  axltwlin  8237  axlttrn  8238  ltleletr  8251  letr  8252  mul32  8299  mul31  8300  add32  8328  subsub23  8374  addsubass  8379  subcan2  8394  subsub2  8397  nppcan2  8400  sub32  8403  nnncan  8404  nnncan2  8406  pnpcan2  8409  subdi  8554  subdir  8555  reapcotr  8768  receuap  8839  divmulap3  8847  divrecap  8858  divrecap2  8859  divsubdirap  8878  divdivap1  8893  redivclap  8901  div2negap  8905  ltmul2  9026  lemul2  9027  lemul2a  9029  lediv1  9039  gt0div  9040  ge0div  9041  ltdivmul  9046  ltdivmul2  9048  ledivmul2  9050  uzind2  9582  nn0ind  9584  fnn0ind  9586  uz3m2nn  9797  xrletr  10033  xrre2  10046  xleadd2a  10099  xleadd1  10100  xltadd2  10102  ixxdisj  10128  iooneg  10213  iccneg  10214  icoshft  10215  icoshftf1o  10216  icodisj  10217  fzen  10268  fzrev3  10312  2ffzeq  10366  fzoaddel2  10425  elfzodifsumelfzo  10436  ssfzo12bi  10460  fzoshftral  10474  adddivflid  10542  fldiv4p1lem1div2  10555  modqmulnn  10594  modqeqmodmin  10646  frec2uzf1od  10658  expdivap  10842  ccatval1  11164  ccatass  11175  fzowrddc  11218  swrdval  11219  swrdnd  11230  swrd0g  11231  swrdfv2  11234  pfxsuff1eqwrdeq  11270  swrdswrdlem  11275  pfxccatin12lem2a  11298  pfxccatin12lem1  11299  shftval2  11377  mulreap  11415  absdivap  11621  absdiflt  11643  absdifle  11644  abs3dif  11656  cau3  11666  ltmininf  11786  xrmaxlesup  11810  xrltmininf  11821  xrlemininf  11822  xrminltinf  11823  geoisum1c  12071  dvdsmulc  12370  dvdsmultr1  12382  dvdsmultr2  12384  dvdssub2  12386  oexpneg  12428  divalgb  12476  ndvdsadd  12482  gcdaddm  12545  modgcd  12552  dvdsgcd  12573  dvdsgcdb  12574  gcdass  12576  mulgcd  12577  absmulgcd  12578  rpmulgcd  12587  nn0seqcvgd  12603  algcvga  12613  lcmdvds  12641  lcmdvdsb  12646  lcmass  12647  coprmdvds  12654  coprmdvds2  12655  rpmul  12660  cncongr1  12665  cncongr2  12666  prmgt1  12694  qnumdenbi  12754  coprimeprodsq  12820  pythagtriplem4  12831  pythagtriplem8  12835  pythagtriplem9  12836  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pcpremul  12856  pcgcd  12892  setsvala  13103  setsex  13104  ressval2  13139  isgrpi  13597  grpsubrcan  13654  grpinvsub  13655  grpsubeq0  13659  grpsubadd0sub  13660  grpnpcan  13665  qussub  13814  ghmsub  13828  opprmulg  14074  rrgeq0  14269  lmodvsubval2  14346  rmodislmodlem  14354  rmodislmod  14355  lssintclm  14388  lssincl  14389  rnglidlmmgm  14500  cncrng  14573  unopn  14719  clsss  14832  opnssneib  14870  restabs  14889  upxp  14986  blpnfctr  15153  mscl  15179  xmscl  15180  xmsge0  15181  xmseq0  15182  mpomulcn  15280  rpdivcxp  15625  cxpcom  15652  rplogbreexp  15667  rplogbzexp  15668  rprelogbmulexp  15670  logbleb  15675  logblt  15676  lgsneg  15743  lgsne0  15757  lgsmodeq  15764  lgsmulsqcoprm  15765  gausslemma2dlem1a  15777  funvtxdm2domval  15870  funiedgdm2domval  15871  iedgedgg  15902  iswlk  16120  uspgr2wlkeq  16162  uspgr2wlkeq2  16163  uspgr2wlkeqi  16164  istrl  16180  clwwlkgt0  16191  iseupth  16242  bj-peano4  16486