Theorem 3adant1 1046

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant2  1050  3ad2ant3  1051  rsp2e  2601  sbciegft  3082  reuhyp  4620  suc11g  4706  soinxp  4847  breldmg  4989  funopg  5414  funimaexglem  5467  fex2  5559  fnreseql  5822  ftpg  5902  mpoeq3ia  6156  funexw  6345  mpofvex  6445  poxp  6472  suppval1  6483  smores3  6569  tfrlemibxssdm  6603  nndi  6764  nnmass  6765  nndir  6768  fnsnsplitdc  6783  nnaord  6787  nnaordr  6788  nnawordi  6793  nnmord  6795  ecopovtrn  6911  ecopovtrng  6914  ixpf  7008  f1oen4g  7044  f1dom4g  7045  mapxpen  7154  netap  7626  2omotaplemap  7629  ltsopi  7693  addassnqg  7755  ltsonq  7771  ltmnqg  7774  distrnq0  7832  addlocpr  7909  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  ltpopr  7968  ltsopr  7969  addcanprg  7989  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulextsr1lem  8153  mulextsr1  8154  axpre-mulext  8261  adddir  8323  axltwlin  8399  axlttrn  8400  ltleletr  8413  letr  8414  mul32  8463  mul31  8464  add32  8492  subsub23  8538  addsubass  8543  subcan2  8558  subsub2  8561  nppcan2  8564  sub32  8567  nnncan  8568  nnncan2  8570  pnpcan2  8573  subdi  8719  subdir  8720  reapcotr  8934  receuap  9007  divmulap3  9015  divrecap  9026  divrecap2  9027  divsubdirap  9046  divdivap1  9061  redivclap  9069  div2negap  9073  ltmul2  9194  lemul2  9195  lemul2a  9197  lediv1  9207  gt0div  9208  ge0div  9209  ltdivmul  9214  ltdivmul2  9216  ledivmul2  9218  uzind2  9768  nn0ind  9770  fnn0ind  9772  uz3m2nn  9988  xrletr  10226  xrre2  10239  xleadd2a  10292  xleadd1  10293  xltadd2  10295  ixxdisj  10321  iooneg  10406  iccneg  10407  icoshft  10408  icoshftf1o  10409  icodisj  10410  fzen  10463  fzrev3  10510  2ffzeq  10564  fzoaddel2  10624  elfzodifsumelfzo  10635  ssfzo12bi  10659  fzoshftral  10673  adddivflid  10747  fldiv4p1lem1div2  10760  modqmulnn  10799  modqeqmodmin  10851  frec2uzf1od  10863  expdivap  11047  ccatval1  11386  ccatass  11397  fzowrddc  11440  swrdval  11441  swrdnd  11452  swrd0g  11453  swrdfv2  11456  pfxsuff1eqwrdeq  11492  swrdswrdlem  11497  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  shftval2  11612  mulreap  11650  absdivap  11857  absdiflt  11880  absdifle  11881  abs3dif  11893  cau3  11903  ltmininf  12024  xrmaxlesup  12049  xrltmininf  12060  xrlemininf  12061  xrminltinf  12062  geoisum1c  12311  dvdsmulc  12610  dvdsmultr1  12622  dvdsmultr2  12624  dvdssub2  12626  oexpneg  12668  divalgb  12716  ndvdsadd  12722  gcdaddm  12785  modgcd  12792  dvdsgcd  12813  dvdsgcdb  12814  gcdass  12816  mulgcd  12817  absmulgcd  12818  rpmulgcd  12827  nn0seqcvgd  12843  algcvga  12853  lcmdvds  12881  lcmdvdsb  12886  lcmass  12887  coprmdvds  12894  coprmdvds2  12895  rpmul  12900  cncongr1  12905  cncongr2  12906  prmgt1  12935  qnumdenbi  12996  coprimeprodsq  13064  pythagtriplem4  13075  pythagtriplem8  13079  pythagtriplem9  13080  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  pcpremul  13100  pcgcd  13136  setsvala  13440  setsex  13441  ressval2  13478  isgrpi  13887  grpsubrcan  13944  grpinvsub  13945  grpsubeq0  13949  grpsubadd0sub  13950  grpnpcan  13955  qussub  14098  ghmsub  14112  opprmulg  14484  rrgeq0  14681  lmodvsubval2  14787  rmodislmodlem  14795  rmodislmod  14796  lssintclm  14829  lssincl  14830  rnglidlmmgm  14941  cncrng  15014  unopn  15248  clsss  15361  opnssneib  15399  restabs  15418  upxp  15515  blpnfctr  15682  mscl  15708  xmscl  15709  xmsge0  15710  xmseq0  15711  mpomulcn  15809  rpdivcxp  16161  cxpcom  16190  rplogbreexp  16206  rplogbzexp  16207  rprelogbmulexp  16209  logbleb  16214  logblt  16215  lgsneg  16365  lgsne0  16379  lgsmodeq  16386  lgsmulsqcoprm  16387  gausslemma2dlem1a  16399  funvtxdm2domval  16492  funiedgdm2domval  16493  iedgedgg  16524  iswlk  16786  uspgr2wlkeq  16828  uspgr2wlkeq2  16829  uspgr2wlkeqi  16830  istrl  16848  clwwlkgt0  16859  iseupth  16910  bj-peano4  17203