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  5837  mpoeq3ia  6085  funexw  6273  mpofvex  6369  poxp  6396  smores3  6458  tfrlemibxssdm  6492  nndi  6653  nnmass  6654  nndir  6657  fnsnsplitdc  6672  nnaord  6676  nnaordr  6677  nnawordi  6682  nnmord  6684  ecopovtrn  6800  ecopovtrng  6803  ixpf  6888  f1oen4g  6924  f1dom4g  6925  mapxpen  7033  netap  7472  2omotaplemap  7475  ltsopi  7539  addassnqg  7601  ltsonq  7617  ltmnqg  7620  distrnq0  7678  addlocpr  7755  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  ltpopr  7814  ltsopr  7815  addcanprg  7835  lttrsr  7981  ltsosr  7983  ltasrg  7989  recexgt0sr  7992  mulextsr1lem  7999  mulextsr1  8000  axpre-mulext  8107  adddir  8169  axltwlin  8246  axlttrn  8247  ltleletr  8260  letr  8261  mul32  8308  mul31  8309  add32  8337  subsub23  8383  addsubass  8388  subcan2  8403  subsub2  8406  nppcan2  8409  sub32  8412  nnncan  8413  nnncan2  8415  pnpcan2  8418  subdi  8563  subdir  8564  reapcotr  8777  receuap  8848  divmulap3  8856  divrecap  8867  divrecap2  8868  divsubdirap  8887  divdivap1  8902  redivclap  8910  div2negap  8914  ltmul2  9035  lemul2  9036  lemul2a  9038  lediv1  9048  gt0div  9049  ge0div  9050  ltdivmul  9055  ltdivmul2  9057  ledivmul2  9059  uzind2  9591  nn0ind  9593  fnn0ind  9595  uz3m2nn  9806  xrletr  10042  xrre2  10055  xleadd2a  10108  xleadd1  10109  xltadd2  10111  ixxdisj  10137  iooneg  10222  iccneg  10223  icoshft  10224  icoshftf1o  10225  icodisj  10226  fzen  10277  fzrev3  10321  2ffzeq  10375  fzoaddel2  10434  elfzodifsumelfzo  10445  ssfzo12bi  10469  fzoshftral  10483  adddivflid  10551  fldiv4p1lem1div2  10564  modqmulnn  10603  modqeqmodmin  10655  frec2uzf1od  10667  expdivap  10851  ccatval1  11173  ccatass  11184  fzowrddc  11227  swrdval  11228  swrdnd  11239  swrd0g  11240  swrdfv2  11243  pfxsuff1eqwrdeq  11279  swrdswrdlem  11284  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  shftval2  11386  mulreap  11424  absdivap  11630  absdiflt  11652  absdifle  11653  abs3dif  11665  cau3  11675  ltmininf  11795  xrmaxlesup  11819  xrltmininf  11830  xrlemininf  11831  xrminltinf  11832  geoisum1c  12080  dvdsmulc  12379  dvdsmultr1  12391  dvdsmultr2  12393  dvdssub2  12395  oexpneg  12437  divalgb  12485  ndvdsadd  12491  gcdaddm  12554  modgcd  12561  dvdsgcd  12582  dvdsgcdb  12583  gcdass  12585  mulgcd  12586  absmulgcd  12587  rpmulgcd  12596  nn0seqcvgd  12612  algcvga  12622  lcmdvds  12650  lcmdvdsb  12655  lcmass  12656  coprmdvds  12663  coprmdvds2  12664  rpmul  12669  cncongr1  12674  cncongr2  12675  prmgt1  12703  qnumdenbi  12763  coprimeprodsq  12829  pythagtriplem4  12840  pythagtriplem8  12844  pythagtriplem9  12845  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pcpremul  12865  pcgcd  12901  setsvala  13112  setsex  13113  ressval2  13148  isgrpi  13606  grpsubrcan  13663  grpinvsub  13664  grpsubeq0  13668  grpsubadd0sub  13669  grpnpcan  13674  qussub  13823  ghmsub  13837  opprmulg  14083  rrgeq0  14278  lmodvsubval2  14355  rmodislmodlem  14363  rmodislmod  14364  lssintclm  14397  lssincl  14398  rnglidlmmgm  14509  cncrng  14582  unopn  14728  clsss  14841  opnssneib  14879  restabs  14898  upxp  14995  blpnfctr  15162  mscl  15188  xmscl  15189  xmsge0  15190  xmseq0  15191  mpomulcn  15289  rpdivcxp  15634  cxpcom  15661  rplogbreexp  15676  rplogbzexp  15677  rprelogbmulexp  15679  logbleb  15684  logblt  15685  lgsneg  15752  lgsne0  15766  lgsmodeq  15773  lgsmulsqcoprm  15774  gausslemma2dlem1a  15786  funvtxdm2domval  15879  funiedgdm2domval  15880  iedgedgg  15911  iswlk  16173  uspgr2wlkeq  16215  uspgr2wlkeq2  16216  uspgr2wlkeqi  16217  istrl  16235  clwwlkgt0  16246  iseupth  16297  bj-peano4  16550