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  2162  vtoclegft  2888  eqeu  2986  ifnebibdc  3667  suc11g  4678  soinxp  4819  funopg  5385  fnco  5465  dff1o2  5618  fnimapr  5736  fvun1  5742  fvmptt  5768  fnreseql  5787  fvpr1g  5889  fvpr2g  5890  f1elima  5945  f1ocnvfvb  5952  ovexg  6083  oprssov  6195  poxp  6427  smoiso  6532  rdgivallem  6611  nndi  6718  nndir  6722  fnsnsplitdc  6737  nnaord  6741  nnaordr  6742  nnaword  6743  nnawordi  6747  ecopovtrn  6865  ecopovtrng  6868  mapsnd  6922  xpdom3m  7084  mapxpen  7100  findcard  7144  fisseneq  7194  resfnfinfinss  7205  funrnfi  7208  netap  7567  2omotaplemap  7570  ltsopi  7634  addcanpig  7648  addassnqg  7696  distrnqg  7701  ltsonq  7712  ltmnqg  7715  prarloclemarch2  7733  nnanq0  7772  distrnq0  7773  distnq0r  7777  prltlu  7801  prarloclem5  7814  distrlem1prl  7896  distrlem1pru  7897  distrlem5prl  7900  distrlem5pru  7901  ltpopr  7909  ltsopr  7910  ltexprlemm  7914  ltexprlemfl  7923  ltexprlemfu  7925  lttrsr  8076  ltsosr  8078  ltasrg  8084  recexgt0sr  8087  mulextsr1lem  8094  mulextsr1  8095  axpre-mulext  8202  adddir  8264  axltwlin  8340  axlttrn  8341  ltleletr  8354  letr  8355  nnncan1  8508  npncan3  8510  pnpcan2  8512  subdi  8657  subdir  8658  reapcotr  8871  divmulap  8948  div23ap  8964  div13ap  8966  muldivdirap  8980  divsubdirap  8981  divcanap7  8994  ltmul2  9129  lemul2  9130  lemul2a  9132  lediv1  9142  ltmuldiv2  9148  lemuldiv2  9155  squeeze0  9177  nndivtr  9278  bndndx  9494  nn0n0n1ge2  9647  fnn0ind  9693  addlelt  10100  xrletr  10140  xrltne  10145  xleadd2a  10206  xleadd1  10207  xltadd2  10209  iooneg  10320  iccneg  10321  icoshft  10322  icoshftf1o  10323  zltaddlt1le  10340  fztri3or  10372  fzdcel  10373  fzen  10376  uzsubsubfz  10380  fzrevral2  10439  fzshftral  10441  fz0fzdiffz0  10463  elfzmlbp  10465  elfzo  10482  nelfzo  10485  fzoaddel2  10534  fzosubel2  10539  elfzom1p1elfzo  10558  ssfzo12bi  10569  subfzo0  10587  flltdivnn0lt  10663  modqmulnn  10703  modfzo0difsn  10756  expdivap  10951  expubnd  10957  mulbinom2  11017  bernneq2  11022  ccatval1  11281  ccatval3  11283  ccatfv0  11287  ccatval1lsw  11288  ccatws1lenp1bg  11319  pfxsuffeqwrdeq  11386  pfxsuff1eqwrdeq  11387  swrdswrd  11393  pfxpfx  11396  wrd2ind  11411  swrdccatin1  11413  pfxccatin12lem1  11416  swrdccatin2  11417  pfxccatin12lem3  11420  swrdccat  11423  pfxccatpfx1  11424  pfxccatpfx2  11425  swrdccat3blem  11427  shftuz  11498  shftval2  11507  abs3dif  11786  xrmaxlesup  11940  xrltmininf  11951  xrlemininf  11952  sin02gt0  12446  dvdsval2  12472  dvdscmul  12500  dvdsmulc  12501  ndvdssub  12612  rpmulgcd  12718  cncongr1  12796  cncongr2  12797  isprm3  12811  coprimeprodsq  12951  pythagtriplem12  12969  pythagtriplem14  12971  pcmul  12995  pcdiv  12996  pcqcl  13000  pcqdiv  13001  pcdvdsb  13014  ercpbl  13536  mgmb1mgm1  13573  grpinvid1  13757  grpinvid2  13758  grpasscan1  13768  grpasscan2  13769  grpinvadd  13783  grpsubf  13784  grpsubrcan  13786  grpinvsub  13787  grpsubeq0  13791  grpsubadd0sub  13792  grppncan  13796  grpnpcan  13797  mulgnn0p1  13842  mulgaddcomlem  13854  mulginvcom  13856  mulginvinv  13857  subgsubcl  13894  subgsub  13895  eqglact  13934  quselbasg  13939  quseccl0g  13940  qussub  13946  ghmsub  13960  subcmnd  14042  srg1zr  14123  dvrcl  14272  unitdvcl  14273  dvrcan1  14277  dvrcan3  14278  dvreq1  14279  subrgdv  14375  lmodvsubval2  14482  lmodprop2d  14488  zndvds  14789  ntrin  14981  elnei  15009  cnrest2  15093  psmetsym  15186  psmetge0  15188  xmetge0  15222  xmetsym  15225  cnmet  15387  rpcxpsub  15765  rpdivcxp  15768  logbleb  15818  logblt  15819  lgsmodeq  15910  lgsmulsqcoprm  15911  gausslemma2dlem1a  15923  2lgsoddprmlem2  15971  upgrpredgv  16133  issubgr2  16245  uhgrissubgr  16248  egrsubgr  16250  upgrwlkvtxedg  16351  clwwlk1loop  16386  clwwlkccatlem  16387  clwwlknonex2lem2  16425  bj-peano4  16717