Theorem 3adant1 1041

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

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

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 1006

This theorem is referenced by:  3ad2ant2  1045  3ad2ant3  1046  rsp2e  2583  sbciegft  3062  reuhyp  4569  suc11g  4655  soinxp  4796  breldmg  4937  funopg  5360  funimaexglem  5413  fex2  5503  fnreseql  5757  ftpg  5838  mpoeq3ia  6086  funexw  6274  mpofvex  6370  poxp  6397  smores3  6459  tfrlemibxssdm  6493  nndi  6654  nnmass  6655  nndir  6658  fnsnsplitdc  6673  nnaord  6677  nnaordr  6678  nnawordi  6683  nnmord  6685  ecopovtrn  6801  ecopovtrng  6804  ixpf  6889  f1oen4g  6925  f1dom4g  6926  mapxpen  7034  netap  7473  2omotaplemap  7476  ltsopi  7540  addassnqg  7602  ltsonq  7618  ltmnqg  7621  distrnq0  7679  addlocpr  7756  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltpopr  7815  ltsopr  7816  addcanprg  7836  lttrsr  7982  ltsosr  7984  ltasrg  7990  recexgt0sr  7993  mulextsr1lem  8000  mulextsr1  8001  axpre-mulext  8108  adddir  8170  axltwlin  8247  axlttrn  8248  ltleletr  8261  letr  8262  mul32  8309  mul31  8310  add32  8338  subsub23  8384  addsubass  8389  subcan2  8404  subsub2  8407  nppcan2  8410  sub32  8413  nnncan  8414  nnncan2  8416  pnpcan2  8419  subdi  8564  subdir  8565  reapcotr  8778  receuap  8849  divmulap3  8857  divrecap  8868  divrecap2  8869  divsubdirap  8888  divdivap1  8903  redivclap  8911  div2negap  8915  ltmul2  9036  lemul2  9037  lemul2a  9039  lediv1  9049  gt0div  9050  ge0div  9051  ltdivmul  9056  ltdivmul2  9058  ledivmul2  9060  uzind2  9592  nn0ind  9594  fnn0ind  9596  uz3m2nn  9807  xrletr  10043  xrre2  10056  xleadd2a  10109  xleadd1  10110  xltadd2  10112  ixxdisj  10138  iooneg  10223  iccneg  10224  icoshft  10225  icoshftf1o  10226  icodisj  10227  fzen  10278  fzrev3  10322  2ffzeq  10376  fzoaddel2  10436  elfzodifsumelfzo  10447  ssfzo12bi  10471  fzoshftral  10485  adddivflid  10553  fldiv4p1lem1div2  10566  modqmulnn  10605  modqeqmodmin  10657  frec2uzf1od  10669  expdivap  10853  ccatval1  11178  ccatass  11189  fzowrddc  11232  swrdval  11233  swrdnd  11244  swrd0g  11245  swrdfv2  11248  pfxsuff1eqwrdeq  11284  swrdswrdlem  11289  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  shftval2  11404  mulreap  11442  absdivap  11648  absdiflt  11670  absdifle  11671  abs3dif  11683  cau3  11693  ltmininf  11813  xrmaxlesup  11837  xrltmininf  11848  xrlemininf  11849  xrminltinf  11850  geoisum1c  12099  dvdsmulc  12398  dvdsmultr1  12410  dvdsmultr2  12412  dvdssub2  12414  oexpneg  12456  divalgb  12504  ndvdsadd  12510  gcdaddm  12573  modgcd  12580  dvdsgcd  12601  dvdsgcdb  12602  gcdass  12604  mulgcd  12605  absmulgcd  12606  rpmulgcd  12615  nn0seqcvgd  12631  algcvga  12641  lcmdvds  12669  lcmdvdsb  12674  lcmass  12675  coprmdvds  12682  coprmdvds2  12683  rpmul  12688  cncongr1  12693  cncongr2  12694  prmgt1  12722  qnumdenbi  12782  coprimeprodsq  12848  pythagtriplem4  12859  pythagtriplem8  12863  pythagtriplem9  12864  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pcpremul  12884  pcgcd  12920  setsvala  13131  setsex  13132  ressval2  13167  isgrpi  13625  grpsubrcan  13682  grpinvsub  13683  grpsubeq0  13687  grpsubadd0sub  13688  grpnpcan  13693  qussub  13842  ghmsub  13856  opprmulg  14103  rrgeq0  14298  lmodvsubval2  14375  rmodislmodlem  14383  rmodislmod  14384  lssintclm  14417  lssincl  14418  rnglidlmmgm  14529  cncrng  14602  unopn  14748  clsss  14861  opnssneib  14899  restabs  14918  upxp  15015  blpnfctr  15182  mscl  15208  xmscl  15209  xmsge0  15210  xmseq0  15211  mpomulcn  15309  rpdivcxp  15654  cxpcom  15681  rplogbreexp  15696  rplogbzexp  15697  rprelogbmulexp  15699  logbleb  15704  logblt  15705  lgsneg  15772  lgsne0  15786  lgsmodeq  15793  lgsmulsqcoprm  15794  gausslemma2dlem1a  15806  funvtxdm2domval  15899  funiedgdm2domval  15900  iedgedgg  15931  iswlk  16193  uspgr2wlkeq  16235  uspgr2wlkeq2  16236  uspgr2wlkeqi  16237  istrl  16255  clwwlkgt0  16266  iseupth  16317  bj-peano4  16601