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  2990  ifnebibdc  3672  suc11g  4684  soinxp  4825  funopg  5391  fnco  5471  dff1o2  5624  fnimapr  5742  fvun1  5748  fvmptt  5774  fnreseql  5793  fvpr1g  5895  fvpr2g  5896  f1elima  5952  f1ocnvfvb  5959  ovexg  6092  oprssov  6204  poxp  6441  smoiso  6546  rdgivallem  6625  nndi  6732  nndir  6736  fnsnsplitdc  6751  nnaord  6755  nnaordr  6756  nnaword  6757  nnawordi  6761  ecopovtrn  6879  ecopovtrng  6882  mapsnd  6936  xpdom3m  7098  mapxpen  7114  findcard  7158  fisseneq  7208  resfnfinfinss  7219  funrnfi  7222  netap  7584  2omotaplemap  7587  ltsopi  7651  addcanpig  7665  addassnqg  7713  distrnqg  7718  ltsonq  7729  ltmnqg  7732  prarloclemarch2  7750  nnanq0  7789  distrnq0  7790  distnq0r  7794  prltlu  7818  prarloclem5  7831  distrlem1prl  7913  distrlem1pru  7914  distrlem5prl  7917  distrlem5pru  7918  ltpopr  7926  ltsopr  7927  ltexprlemm  7931  ltexprlemfl  7940  ltexprlemfu  7942  lttrsr  8093  ltsosr  8095  ltasrg  8101  recexgt0sr  8104  mulextsr1lem  8111  mulextsr1  8112  axpre-mulext  8219  adddir  8281  axltwlin  8357  axlttrn  8358  ltleletr  8371  letr  8372  nnncan1  8525  npncan3  8527  pnpcan2  8529  subdi  8675  subdir  8676  reapcotr  8889  divmulap  8966  div23ap  8982  div13ap  8984  muldivdirap  8998  divsubdirap  8999  divcanap7  9012  ltmul2  9147  lemul2  9148  lemul2a  9150  lediv1  9160  ltmuldiv2  9166  lemuldiv2  9173  squeeze0  9195  nndivtr  9296  bndndx  9512  nn0n0n1ge2  9665  fnn0ind  9712  addlelt  10119  xrletr  10160  xrltne  10165  xleadd2a  10226  xleadd1  10227  xltadd2  10229  iooneg  10340  iccneg  10341  icoshft  10342  icoshftf1o  10343  zltaddlt1le  10360  fztri3or  10393  fzdcel  10394  fzen  10397  uzsubsubfz  10401  fzrevral2  10462  fzshftral  10464  fz0fzdiffz0  10486  elfzmlbp  10488  elfzo  10505  nelfzo  10508  fzoaddel2  10557  fzosubel2  10562  elfzom1p1elfzo  10581  ssfzo12bi  10592  subfzo0  10610  flltdivnn0lt  10688  modqmulnn  10728  modfzo0difsn  10781  expdivap  10976  expubnd  10982  mulbinom2  11042  bernneq2  11048  ccatval1  11310  ccatval3  11312  ccatfv0  11316  ccatval1lsw  11317  ccatws1lenp1bg  11348  pfxsuffeqwrdeq  11415  pfxsuff1eqwrdeq  11416  swrdswrd  11422  pfxpfx  11425  wrd2ind  11440  swrdccatin1  11442  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem3  11449  swrdccat  11452  pfxccatpfx1  11453  pfxccatpfx2  11454  swrdccat3blem  11456  shftuz  11527  shftval2  11536  abs3dif  11815  xrmaxlesup  11969  xrltmininf  11980  xrlemininf  11981  sin02gt0  12475  dvdsval2  12501  dvdscmul  12529  dvdsmulc  12530  ndvdssub  12641  rpmulgcd  12747  cncongr1  12825  cncongr2  12826  isprm3  12840  coprimeprodsq  12980  pythagtriplem12  12998  pythagtriplem14  13000  pcmul  13024  pcdiv  13025  pcqcl  13029  pcqdiv  13030  pcdvdsb  13043  ercpbl  13628  mgmb1mgm1  13665  grpinvid1  13849  grpinvid2  13850  grpasscan1  13860  grpasscan2  13861  grpinvadd  13875  grpsubf  13876  grpsubrcan  13878  grpinvsub  13879  grpsubeq0  13883  grpsubadd0sub  13884  grppncan  13888  grpnpcan  13889  mulgnn0p1  13934  mulgaddcomlem  13946  mulginvcom  13948  mulginvinv  13949  subgsubcl  13986  subgsub  13987  eqglact  14026  quselbasg  14031  quseccl0g  14032  qussub  14038  ghmsub  14052  subcmnd  14134  srg1zr  14215  dvrcl  14365  unitdvcl  14366  dvrcan1  14370  dvrcan3  14371  dvreq1  14372  subrgdv  14469  lmodvsubval2  14602  lmodprop2d  14608  zndvds  14909  ntrin  15101  elnei  15129  cnrest2  15213  psmetsym  15306  psmetge0  15308  xmetge0  15342  xmetsym  15345  cnmet  15507  rpcxpsub  15885  rpdivcxp  15888  logbleb  15938  logblt  15939  lgsmodeq  16030  lgsmulsqcoprm  16031  gausslemma2dlem1a  16043  2lgsoddprmlem2  16091  upgrpredgv  16253  issubgr2  16365  uhgrissubgr  16368  egrsubgr  16370  upgrwlkvtxedg  16471  clwwlk1loop  16506  clwwlkccatlem  16507  clwwlknonex2lem2  16545  bj-peano4  16837