Theorem 3adant2 1047

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

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

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 1011

This theorem is referenced by:  3ad2ant1  1049  3imp3i2an  1214  eupickb  2168  vtoclegft  2897  eqeu  2996  ifnebibdc  3686  suc11g  4702  soinxp  4843  funopg  5409  fnco  5489  dff1o2  5642  fnimapr  5760  fvun1  5766  fvmptt  5794  fnreseql  5813  fvpr1g  5915  fvpr2g  5916  f1elima  5973  f1ocnvfvb  5980  ovexg  6113  oprssov  6225  poxp  6462  smoiso  6567  rdgivallem  6646  nndi  6753  nndir  6757  fnsnsplitdc  6772  nnaord  6776  nnaordr  6777  nnaword  6778  nnawordi  6782  ecopovtrn  6900  ecopovtrng  6903  mapsnd  6964  xpdom3m  7126  mapxpen  7142  findcard  7186  fisseneq  7236  resfnfinfinss  7247  funrnfi  7250  netap  7614  2omotaplemap  7617  ltsopi  7681  addcanpig  7695  addassnqg  7743  distrnqg  7748  ltsonq  7759  ltmnqg  7762  prarloclemarch2  7780  nnanq0  7819  distrnq0  7820  distnq0r  7824  prltlu  7848  prarloclem5  7861  distrlem1prl  7943  distrlem1pru  7944  distrlem5prl  7947  distrlem5pru  7948  ltpopr  7956  ltsopr  7957  ltexprlemm  7961  ltexprlemfl  7970  ltexprlemfu  7972  lttrsr  8123  ltsosr  8125  ltasrg  8131  recexgt0sr  8134  mulextsr1lem  8141  mulextsr1  8142  axpre-mulext  8249  adddir  8311  axltwlin  8387  axlttrn  8388  ltleletr  8401  letr  8402  nnncan1  8556  npncan3  8558  pnpcan2  8560  subdi  8706  subdir  8707  reapcotr  8920  divmulap  8999  div23ap  9015  div13ap  9017  muldivdirap  9031  divsubdirap  9032  divcanap7  9045  ltmul2  9180  lemul2  9181  lemul2a  9183  lediv1  9193  ltmuldiv2  9199  lemuldiv2  9206  squeeze0  9228  nndivtr  9329  bndndx  9545  nn0n0n1ge2  9698  fnn0ind  9745  addlelt  10152  xrletr  10193  xrltne  10198  xleadd2a  10259  xleadd1  10260  xltadd2  10262  iooneg  10373  iccneg  10374  icoshft  10375  icoshftf1o  10376  zltaddlt1le  10393  fztri3or  10426  fzdcel  10427  fzen  10430  uzsubsubfz  10435  fzrevral2  10496  fzshftral  10498  fz0fzdiffz0  10520  elfzmlbp  10522  elfzo  10539  nelfzo  10542  fzoaddel2  10591  fzosubel2  10596  elfzom1p1elfzo  10615  ssfzo12bi  10626  subfzo0  10644  flltdivnn0lt  10722  modqmulnn  10762  modfzo0difsn  10815  expdivap  11010  expubnd  11016  mulbinom2  11076  bernneq2  11082  ccatval1  11348  ccatval3  11350  ccatfv0  11354  ccatval1lsw  11355  ccatws1lenp1bg  11386  pfxsuffeqwrdeq  11453  pfxsuff1eqwrdeq  11454  swrdswrd  11460  pfxpfx  11463  wrd2ind  11478  swrdccatin1  11480  pfxccatin12lem1  11483  swrdccatin2  11484  pfxccatin12lem3  11487  swrdccat  11490  pfxccatpfx1  11491  pfxccatpfx2  11492  swrdccat3blem  11494  shftuz  11565  shftval2  11574  abs3dif  11854  xrmaxlesup  12008  xrltmininf  12019  xrlemininf  12020  sin02gt0  12514  dvdsval2  12540  dvdscmul  12568  dvdsmulc  12569  ndvdssub  12680  rpmulgcd  12786  cncongr1  12864  cncongr2  12865  isprm3  12879  coprimeprodsq  13019  pythagtriplem12  13037  pythagtriplem14  13039  pcmul  13063  pcdiv  13064  pcqcl  13068  pcqdiv  13069  pcdvdsb  13082  ercpbl  13635  mgmb1mgm1  13671  grpinvid1  13840  grpinvid2  13841  grpasscan1  13851  grpasscan2  13852  grpinvadd  13866  grpsubf  13867  grpsubrcan  13869  grpinvsub  13870  grpsubeq0  13874  grpsubadd0sub  13875  grppncan  13879  grpnpcan  13880  mulgnn0p1  13919  mulgaddcomlem  13931  mulginvcom  13933  mulginvinv  13934  subgsubcl  13971  subgsub  13972  eqglact  14011  quselbasg  14016  quseccl0g  14017  qussub  14023  ghmsub  14037  subcmnd  14120  rng1zrlem  14241  dvrcl  14425  unitdvcl  14426  dvrcan1  14430  dvrcan3  14431  dvreq1  14432  subrgdv  14529  lmodvsubval2  14662  lmodprop2d  14668  zndvds  14967  ascldimul  15014  ntrin  15208  elnei  15236  cnrest2  15320  psmetsym  15413  psmetge0  15415  xmetge0  15449  xmetsym  15452  cnmet  15614  rpcxpsub  15993  rpdivcxp  15996  logbleb  16046  logblt  16047  lgsmodeq  16147  lgsmulsqcoprm  16148  gausslemma2dlem1a  16160  2lgsoddprmlem2  16208  upgrpredgv  16370  issubgr2  16482  uhgrissubgr  16485  egrsubgr  16487  upgrwlkvtxedg  16588  clwwlk1loop  16623  clwwlkccatlem  16624  clwwlknonex2lem2  16662  bj-peano4  16964