Theorem 3adant2 1043

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant2	⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3simpb 1022	. 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:  3ad2ant1  1045  3imp3i2an  1210  eupickb  2164  vtoclegft  2891  eqeu  2989  ifnebibdc  3670  suc11g  4681  soinxp  4822  funopg  5388  fnco  5468  dff1o2  5621  fnimapr  5739  fvun1  5745  fvmptt  5771  fnreseql  5790  fvpr1g  5892  fvpr2g  5893  f1elima  5948  f1ocnvfvb  5955  ovexg  6086  oprssov  6198  poxp  6430  smoiso  6535  rdgivallem  6614  nndi  6721  nndir  6725  fnsnsplitdc  6740  nnaord  6744  nnaordr  6745  nnaword  6746  nnawordi  6750  ecopovtrn  6868  ecopovtrng  6871  mapsnd  6925  xpdom3m  7087  mapxpen  7103  findcard  7147  fisseneq  7197  resfnfinfinss  7208  funrnfi  7211  netap  7570  2omotaplemap  7573  ltsopi  7637  addcanpig  7651  addassnqg  7699  distrnqg  7704  ltsonq  7715  ltmnqg  7718  prarloclemarch2  7736  nnanq0  7775  distrnq0  7776  distnq0r  7780  prltlu  7804  prarloclem5  7817  distrlem1prl  7899  distrlem1pru  7900  distrlem5prl  7903  distrlem5pru  7904  ltpopr  7912  ltsopr  7913  ltexprlemm  7917  ltexprlemfl  7926  ltexprlemfu  7928  lttrsr  8079  ltsosr  8081  ltasrg  8087  recexgt0sr  8090  mulextsr1lem  8097  mulextsr1  8098  axpre-mulext  8205  adddir  8267  axltwlin  8343  axlttrn  8344  ltleletr  8357  letr  8358  nnncan1  8511  npncan3  8513  pnpcan2  8515  subdi  8660  subdir  8661  reapcotr  8874  divmulap  8951  div23ap  8967  div13ap  8969  muldivdirap  8983  divsubdirap  8984  divcanap7  8997  ltmul2  9132  lemul2  9133  lemul2a  9135  lediv1  9145  ltmuldiv2  9151  lemuldiv2  9158  squeeze0  9180  nndivtr  9281  bndndx  9497  nn0n0n1ge2  9650  fnn0ind  9697  addlelt  10104  xrletr  10144  xrltne  10149  xleadd2a  10210  xleadd1  10211  xltadd2  10213  iooneg  10324  iccneg  10325  icoshft  10326  icoshftf1o  10327  zltaddlt1le  10344  fztri3or  10376  fzdcel  10377  fzen  10380  uzsubsubfz  10384  fzrevral2  10444  fzshftral  10446  fz0fzdiffz0  10468  elfzmlbp  10470  elfzo  10487  nelfzo  10490  fzoaddel2  10539  fzosubel2  10544  elfzom1p1elfzo  10563  ssfzo12bi  10574  subfzo0  10592  flltdivnn0lt  10668  modqmulnn  10708  modfzo0difsn  10761  expdivap  10956  expubnd  10962  mulbinom2  11022  bernneq2  11027  ccatval1  11289  ccatval3  11291  ccatfv0  11295  ccatval1lsw  11296  ccatws1lenp1bg  11327  pfxsuffeqwrdeq  11394  pfxsuff1eqwrdeq  11395  swrdswrd  11401  pfxpfx  11404  wrd2ind  11419  swrdccatin1  11421  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem3  11428  swrdccat  11431  pfxccatpfx1  11432  pfxccatpfx2  11433  swrdccat3blem  11435  shftuz  11506  shftval2  11515  abs3dif  11794  xrmaxlesup  11948  xrltmininf  11959  xrlemininf  11960  sin02gt0  12454  dvdsval2  12480  dvdscmul  12508  dvdsmulc  12509  ndvdssub  12620  rpmulgcd  12726  cncongr1  12804  cncongr2  12805  isprm3  12819  coprimeprodsq  12959  pythagtriplem12  12977  pythagtriplem14  12979  pcmul  13003  pcdiv  13004  pcqcl  13008  pcqdiv  13009  pcdvdsb  13022  ercpbl  13561  mgmb1mgm1  13598  grpinvid1  13782  grpinvid2  13783  grpasscan1  13793  grpasscan2  13794  grpinvadd  13808  grpsubf  13809  grpsubrcan  13811  grpinvsub  13812  grpsubeq0  13816  grpsubadd0sub  13817  grppncan  13821  grpnpcan  13822  mulgnn0p1  13867  mulgaddcomlem  13879  mulginvcom  13881  mulginvinv  13882  subgsubcl  13919  subgsub  13920  eqglact  13959  quselbasg  13964  quseccl0g  13965  qussub  13971  ghmsub  13985  subcmnd  14067  srg1zr  14148  dvrcl  14297  unitdvcl  14298  dvrcan1  14302  dvrcan3  14303  dvreq1  14304  subrgdv  14400  lmodvsubval2  14507  lmodprop2d  14513  zndvds  14814  ntrin  15006  elnei  15034  cnrest2  15118  psmetsym  15211  psmetge0  15213  xmetge0  15247  xmetsym  15250  cnmet  15412  rpcxpsub  15790  rpdivcxp  15793  logbleb  15843  logblt  15844  lgsmodeq  15935  lgsmulsqcoprm  15936  gausslemma2dlem1a  15948  2lgsoddprmlem2  15996  upgrpredgv  16158  issubgr2  16270  uhgrissubgr  16273  egrsubgr  16275  upgrwlkvtxedg  16376  clwwlk1loop  16411  clwwlkccatlem  16412  clwwlknonex2lem2  16450  bj-peano4  16742