Theorem 3adant1 1039

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

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

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 1004

This theorem is referenced by:  3ad2ant2  1043  3ad2ant3  1044  rsp2e  2581  sbciegft  3059  reuhyp  4563  suc11g  4649  soinxp  4789  breldmg  4929  funopg  5352  funimaexglem  5404  fex2  5494  fnreseql  5747  ftpg  5827  mpoeq3ia  6075  funexw  6263  mpofvex  6357  poxp  6384  smores3  6445  tfrlemibxssdm  6479  nndi  6640  nnmass  6641  nndir  6644  fnsnsplitdc  6659  nnaord  6663  nnaordr  6664  nnawordi  6669  nnmord  6671  ecopovtrn  6787  ecopovtrng  6790  ixpf  6875  f1oen4g  6911  f1dom4g  6912  mapxpen  7017  netap  7451  2omotaplemap  7454  ltsopi  7518  addassnqg  7580  ltsonq  7596  ltmnqg  7599  distrnq0  7657  addlocpr  7734  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  ltpopr  7793  ltsopr  7794  addcanprg  7814  lttrsr  7960  ltsosr  7962  ltasrg  7968  recexgt0sr  7971  mulextsr1lem  7978  mulextsr1  7979  axpre-mulext  8086  adddir  8148  axltwlin  8225  axlttrn  8226  ltleletr  8239  letr  8240  mul32  8287  mul31  8288  add32  8316  subsub23  8362  addsubass  8367  subcan2  8382  subsub2  8385  nppcan2  8388  sub32  8391  nnncan  8392  nnncan2  8394  pnpcan2  8397  subdi  8542  subdir  8543  reapcotr  8756  receuap  8827  divmulap3  8835  divrecap  8846  divrecap2  8847  divsubdirap  8866  divdivap1  8881  redivclap  8889  div2negap  8893  ltmul2  9014  lemul2  9015  lemul2a  9017  lediv1  9027  gt0div  9028  ge0div  9029  ltdivmul  9034  ltdivmul2  9036  ledivmul2  9038  uzind2  9570  nn0ind  9572  fnn0ind  9574  uz3m2nn  9780  xrletr  10016  xrre2  10029  xleadd2a  10082  xleadd1  10083  xltadd2  10085  ixxdisj  10111  iooneg  10196  iccneg  10197  icoshft  10198  icoshftf1o  10199  icodisj  10200  fzen  10251  fzrev3  10295  2ffzeq  10349  fzoaddel2  10408  elfzodifsumelfzo  10419  ssfzo12bi  10443  fzoshftral  10456  adddivflid  10524  fldiv4p1lem1div2  10537  modqmulnn  10576  modqeqmodmin  10628  frec2uzf1od  10640  expdivap  10824  ccatval1  11145  ccatass  11156  fzowrddc  11194  swrdval  11195  swrdnd  11206  swrd0g  11207  swrdfv2  11210  pfxsuff1eqwrdeq  11246  swrdswrdlem  11251  pfxccatin12lem2a  11274  pfxccatin12lem1  11275  shftval2  11352  mulreap  11390  absdivap  11596  absdiflt  11618  absdifle  11619  abs3dif  11631  cau3  11641  ltmininf  11761  xrmaxlesup  11785  xrltmininf  11796  xrlemininf  11797  xrminltinf  11798  geoisum1c  12046  dvdsmulc  12345  dvdsmultr1  12357  dvdsmultr2  12359  dvdssub2  12361  oexpneg  12403  divalgb  12451  ndvdsadd  12457  gcdaddm  12520  modgcd  12527  dvdsgcd  12548  dvdsgcdb  12549  gcdass  12551  mulgcd  12552  absmulgcd  12553  rpmulgcd  12562  nn0seqcvgd  12578  algcvga  12588  lcmdvds  12616  lcmdvdsb  12621  lcmass  12622  coprmdvds  12629  coprmdvds2  12630  rpmul  12635  cncongr1  12640  cncongr2  12641  prmgt1  12669  qnumdenbi  12729  coprimeprodsq  12795  pythagtriplem4  12806  pythagtriplem8  12810  pythagtriplem9  12811  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pcpremul  12831  pcgcd  12867  setsvala  13078  setsex  13079  ressval2  13114  isgrpi  13572  grpsubrcan  13629  grpinvsub  13630  grpsubeq0  13634  grpsubadd0sub  13635  grpnpcan  13640  qussub  13789  ghmsub  13803  opprmulg  14049  rrgeq0  14244  lmodvsubval2  14321  rmodislmodlem  14329  rmodislmod  14330  lssintclm  14363  lssincl  14364  rnglidlmmgm  14475  cncrng  14548  unopn  14694  clsss  14807  opnssneib  14845  restabs  14864  upxp  14961  blpnfctr  15128  mscl  15154  xmscl  15155  xmsge0  15156  xmseq0  15157  mpomulcn  15255  rpdivcxp  15600  cxpcom  15627  rplogbreexp  15642  rplogbzexp  15643  rprelogbmulexp  15645  logbleb  15650  logblt  15651  lgsneg  15718  lgsne0  15732  lgsmodeq  15739  lgsmulsqcoprm  15740  gausslemma2dlem1a  15752  funvtxdm2domval  15845  funiedgdm2domval  15846  iedgedgg  15876  iswlk  16064  uspgr2wlkeq  16106  uspgr2wlkeq2  16107  uspgr2wlkeqi  16108  istrl  16124  clwwlkgt0  16134  bj-peano4  16373