Theorem 3adant1 1042

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

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

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 1007

This theorem is referenced by:  3ad2ant2  1046  3ad2ant3  1047  rsp2e  2593  sbciegft  3073  reuhyp  4593  suc11g  4679  soinxp  4820  breldmg  4962  funopg  5386  funimaexglem  5439  fex2  5531  fnreseql  5788  ftpg  5868  mpoeq3ia  6118  funexw  6305  mpofvex  6401  poxp  6428  suppval1  6439  smores3  6524  tfrlemibxssdm  6558  nndi  6719  nnmass  6720  nndir  6723  fnsnsplitdc  6738  nnaord  6742  nnaordr  6743  nnawordi  6748  nnmord  6750  ecopovtrn  6866  ecopovtrng  6869  ixpf  6955  f1oen4g  6991  f1dom4g  6992  mapxpen  7101  funisfsupp  7244  netap  7568  2omotaplemap  7571  ltsopi  7635  addassnqg  7697  ltsonq  7713  ltmnqg  7716  distrnq0  7774  addlocpr  7851  distrlem1prl  7897  distrlem1pru  7898  distrlem4prl  7899  distrlem4pru  7900  ltpopr  7910  ltsopr  7911  addcanprg  7931  lttrsr  8077  ltsosr  8079  ltasrg  8085  recexgt0sr  8088  mulextsr1lem  8095  mulextsr1  8096  axpre-mulext  8203  adddir  8265  axltwlin  8341  axlttrn  8342  ltleletr  8355  letr  8356  mul32  8403  mul31  8404  add32  8432  subsub23  8478  addsubass  8483  subcan2  8498  subsub2  8501  nppcan2  8504  sub32  8507  nnncan  8508  nnncan2  8510  pnpcan2  8513  subdi  8658  subdir  8659  reapcotr  8872  receuap  8943  divmulap3  8951  divrecap  8962  divrecap2  8963  divsubdirap  8982  divdivap1  8997  redivclap  9005  div2negap  9009  ltmul2  9130  lemul2  9131  lemul2a  9133  lediv1  9143  gt0div  9144  ge0div  9145  ltdivmul  9150  ltdivmul2  9152  ledivmul2  9154  uzind2  9690  nn0ind  9692  fnn0ind  9694  uz3m2nn  9905  xrletr  10141  xrre2  10154  xleadd2a  10207  xleadd1  10208  xltadd2  10210  ixxdisj  10236  iooneg  10321  iccneg  10322  icoshft  10323  icoshftf1o  10324  icodisj  10325  fzen  10377  fzrev3  10421  2ffzeq  10475  fzoaddel2  10535  elfzodifsumelfzo  10546  ssfzo12bi  10570  fzoshftral  10584  adddivflid  10652  fldiv4p1lem1div2  10665  modqmulnn  10704  modqeqmodmin  10756  frec2uzf1od  10768  expdivap  10952  ccatval1  11285  ccatass  11296  fzowrddc  11339  swrdval  11340  swrdnd  11351  swrd0g  11352  swrdfv2  11355  pfxsuff1eqwrdeq  11391  swrdswrdlem  11396  pfxccatin12lem2a  11419  pfxccatin12lem1  11420  shftval2  11511  mulreap  11549  absdivap  11755  absdiflt  11777  absdifle  11778  abs3dif  11790  cau3  11800  ltmininf  11920  xrmaxlesup  11944  xrltmininf  11955  xrlemininf  11956  xrminltinf  11957  geoisum1c  12206  dvdsmulc  12505  dvdsmultr1  12517  dvdsmultr2  12519  dvdssub2  12521  oexpneg  12563  divalgb  12611  ndvdsadd  12617  gcdaddm  12680  modgcd  12687  dvdsgcd  12708  dvdsgcdb  12709  gcdass  12711  mulgcd  12712  absmulgcd  12713  rpmulgcd  12722  nn0seqcvgd  12738  algcvga  12748  lcmdvds  12776  lcmdvdsb  12781  lcmass  12782  coprmdvds  12789  coprmdvds2  12790  rpmul  12795  cncongr1  12800  cncongr2  12801  prmgt1  12829  qnumdenbi  12889  coprimeprodsq  12955  pythagtriplem4  12966  pythagtriplem8  12970  pythagtriplem9  12971  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pcpremul  12991  pcgcd  13027  setsvala  13243  setsex  13244  ressval2  13279  isgrpi  13737  grpsubrcan  13794  grpinvsub  13795  grpsubeq0  13799  grpsubadd0sub  13800  grpnpcan  13805  qussub  13954  ghmsub  13968  opprmulg  14215  rrgeq0  14410  lmodvsubval2  14490  rmodislmodlem  14498  rmodislmod  14499  lssintclm  14532  lssincl  14533  rnglidlmmgm  14644  cncrng  14717  unopn  14870  clsss  14983  opnssneib  15021  restabs  15040  upxp  15137  blpnfctr  15304  mscl  15330  xmscl  15331  xmsge0  15332  xmseq0  15333  mpomulcn  15431  rpdivcxp  15776  cxpcom  15803  rplogbreexp  15818  rplogbzexp  15819  rprelogbmulexp  15821  logbleb  15826  logblt  15827  lgsneg  15897  lgsne0  15911  lgsmodeq  15918  lgsmulsqcoprm  15919  gausslemma2dlem1a  15931  funvtxdm2domval  16024  funiedgdm2domval  16025  iedgedgg  16056  iswlk  16318  uspgr2wlkeq  16360  uspgr2wlkeq2  16361  uspgr2wlkeqi  16362  istrl  16380  clwwlkgt0  16391  iseupth  16442  bj-peano4  16725