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  10435  elfzodifsumelfzo  10446  ssfzo12bi  10470  fzoshftral  10484  adddivflid  10552  fldiv4p1lem1div2  10565  modqmulnn  10604  modqeqmodmin  10656  frec2uzf1od  10668  expdivap  10852  ccatval1  11174  ccatass  11185  fzowrddc  11228  swrdval  11229  swrdnd  11240  swrd0g  11241  swrdfv2  11244  pfxsuff1eqwrdeq  11280  swrdswrdlem  11285  pfxccatin12lem2a  11308  pfxccatin12lem1  11309  shftval2  11387  mulreap  11425  absdivap  11631  absdiflt  11653  absdifle  11654  abs3dif  11666  cau3  11676  ltmininf  11796  xrmaxlesup  11820  xrltmininf  11831  xrlemininf  11832  xrminltinf  11833  geoisum1c  12082  dvdsmulc  12381  dvdsmultr1  12393  dvdsmultr2  12395  dvdssub2  12397  oexpneg  12439  divalgb  12487  ndvdsadd  12493  gcdaddm  12556  modgcd  12563  dvdsgcd  12584  dvdsgcdb  12585  gcdass  12587  mulgcd  12588  absmulgcd  12589  rpmulgcd  12598  nn0seqcvgd  12614  algcvga  12624  lcmdvds  12652  lcmdvdsb  12657  lcmass  12658  coprmdvds  12665  coprmdvds2  12666  rpmul  12671  cncongr1  12676  cncongr2  12677  prmgt1  12705  qnumdenbi  12765  coprimeprodsq  12831  pythagtriplem4  12842  pythagtriplem8  12846  pythagtriplem9  12847  pythagtriplem12  12849  pythagtriplem14  12851  pythagtriplem16  12853  pcpremul  12867  pcgcd  12903  setsvala  13114  setsex  13115  ressval2  13150  isgrpi  13608  grpsubrcan  13665  grpinvsub  13666  grpsubeq0  13670  grpsubadd0sub  13671  grpnpcan  13676  qussub  13825  ghmsub  13839  opprmulg  14086  rrgeq0  14281  lmodvsubval2  14358  rmodislmodlem  14366  rmodislmod  14367  lssintclm  14400  lssincl  14401  rnglidlmmgm  14512  cncrng  14585  unopn  14731  clsss  14844  opnssneib  14882  restabs  14901  upxp  14998  blpnfctr  15165  mscl  15191  xmscl  15192  xmsge0  15193  xmseq0  15194  mpomulcn  15292  rpdivcxp  15637  cxpcom  15664  rplogbreexp  15679  rplogbzexp  15680  rprelogbmulexp  15682  logbleb  15687  logblt  15688  lgsneg  15755  lgsne0  15769  lgsmodeq  15776  lgsmulsqcoprm  15777  gausslemma2dlem1a  15789  funvtxdm2domval  15882  funiedgdm2domval  15883  iedgedgg  15914  iswlk  16176  uspgr2wlkeq  16218  uspgr2wlkeq2  16219  uspgr2wlkeqi  16220  istrl  16238  clwwlkgt0  16249  iseupth  16300  bj-peano4  16553