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 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

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

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 1011

This theorem is referenced by:  3ad2ant2  1050  3ad2ant3  1051  rsp2e  2601  sbciegft  3082  reuhyp  4613  suc11g  4699  soinxp  4840  breldmg  4982  funopg  5406  funimaexglem  5459  fex2  5551  fnreseql  5810  ftpg  5890  mpoeq3ia  6143  funexw  6331  mpofvex  6431  poxp  6458  suppval1  6469  smores3  6554  tfrlemibxssdm  6588  nndi  6749  nnmass  6750  nndir  6753  fnsnsplitdc  6768  nnaord  6772  nnaordr  6773  nnawordi  6778  nnmord  6780  ecopovtrn  6896  ecopovtrng  6899  ixpf  6992  f1oen4g  7028  f1dom4g  7029  mapxpen  7138  funisfsupp  7281  netap  7610  2omotaplemap  7613  ltsopi  7677  addassnqg  7739  ltsonq  7755  ltmnqg  7758  distrnq0  7816  addlocpr  7893  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  ltpopr  7952  ltsopr  7953  addcanprg  7973  lttrsr  8119  ltsosr  8121  ltasrg  8127  recexgt0sr  8130  mulextsr1lem  8137  mulextsr1  8138  axpre-mulext  8245  adddir  8307  axltwlin  8383  axlttrn  8384  ltleletr  8397  letr  8398  mul32  8446  mul31  8447  add32  8475  subsub23  8521  addsubass  8526  subcan2  8541  subsub2  8544  nppcan2  8547  sub32  8550  nnncan  8551  nnncan2  8553  pnpcan2  8556  subdi  8702  subdir  8703  reapcotr  8916  receuap  8989  divmulap3  8997  divrecap  9008  divrecap2  9009  divsubdirap  9028  divdivap1  9043  redivclap  9051  div2negap  9055  ltmul2  9176  lemul2  9177  lemul2a  9179  lediv1  9189  gt0div  9190  ge0div  9191  ltdivmul  9196  ltdivmul2  9198  ledivmul2  9200  uzind2  9737  nn0ind  9739  fnn0ind  9741  uz3m2nn  9952  xrletr  10189  xrre2  10202  xleadd2a  10255  xleadd1  10256  xltadd2  10258  ixxdisj  10284  iooneg  10369  iccneg  10370  icoshft  10371  icoshftf1o  10372  icodisj  10373  fzen  10426  fzrev3  10472  2ffzeq  10526  fzoaddel2  10586  elfzodifsumelfzo  10597  ssfzo12bi  10621  fzoshftral  10635  adddivflid  10705  fldiv4p1lem1div2  10718  modqmulnn  10757  modqeqmodmin  10809  frec2uzf1od  10821  expdivap  11005  ccatval1  11343  ccatass  11354  fzowrddc  11397  swrdval  11398  swrdnd  11409  swrd0g  11410  swrdfv2  11413  pfxsuff1eqwrdeq  11449  swrdswrdlem  11454  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  shftval2  11569  mulreap  11607  absdivap  11814  absdiflt  11836  absdifle  11837  abs3dif  11849  cau3  11859  ltmininf  11979  xrmaxlesup  12003  xrltmininf  12014  xrlemininf  12015  xrminltinf  12016  geoisum1c  12265  dvdsmulc  12564  dvdsmultr1  12576  dvdsmultr2  12578  dvdssub2  12580  oexpneg  12622  divalgb  12670  ndvdsadd  12676  gcdaddm  12739  modgcd  12746  dvdsgcd  12767  dvdsgcdb  12768  gcdass  12770  mulgcd  12771  absmulgcd  12772  rpmulgcd  12781  nn0seqcvgd  12797  algcvga  12807  lcmdvds  12835  lcmdvdsb  12840  lcmass  12841  coprmdvds  12848  coprmdvds2  12849  rpmul  12854  cncongr1  12859  cncongr2  12860  prmgt1  12888  qnumdenbi  12948  coprimeprodsq  13014  pythagtriplem4  13025  pythagtriplem8  13029  pythagtriplem9  13030  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  pcpremul  13050  pcgcd  13086  setsvala  13361  setsex  13362  ressval2  13397  isgrpi  13806  grpsubrcan  13863  grpinvsub  13864  grpsubeq0  13868  grpsubadd0sub  13869  grpnpcan  13874  qussub  14017  ghmsub  14031  opprmulg  14349  rrgeq0  14546  lmodvsubval2  14651  rmodislmodlem  14659  rmodislmod  14660  lssintclm  14693  lssincl  14694  rnglidlmmgm  14805  cncrng  14878  unopn  15029  clsss  15142  opnssneib  15180  restabs  15199  upxp  15296  blpnfctr  15463  mscl  15489  xmscl  15490  xmsge0  15491  xmseq0  15492  mpomulcn  15590  rpdivcxp  15936  cxpcom  15963  rplogbreexp  15978  rplogbzexp  15979  rprelogbmulexp  15981  logbleb  15986  logblt  15987  lgsneg  16057  lgsne0  16071  lgsmodeq  16078  lgsmulsqcoprm  16079  gausslemma2dlem1a  16091  funvtxdm2domval  16184  funiedgdm2domval  16185  iedgedgg  16216  iswlk  16478  uspgr2wlkeq  16520  uspgr2wlkeq2  16521  uspgr2wlkeqi  16522  istrl  16540  clwwlkgt0  16551  iseupth  16602  bj-peano4  16895