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  8526  npncan3  8528  pnpcan2  8530  subdi  8676  subdir  8677  reapcotr  8890  divmulap  8969  div23ap  8985  div13ap  8987  muldivdirap  9001  divsubdirap  9002  divcanap7  9015  ltmul2  9150  lemul2  9151  lemul2a  9153  lediv1  9163  ltmuldiv2  9169  lemuldiv2  9176  squeeze0  9198  nndivtr  9299  bndndx  9515  nn0n0n1ge2  9668  fnn0ind  9715  addlelt  10122  xrletr  10163  xrltne  10168  xleadd2a  10229  xleadd1  10230  xltadd2  10232  iooneg  10343  iccneg  10344  icoshft  10345  icoshftf1o  10346  zltaddlt1le  10363  fztri3or  10396  fzdcel  10397  fzen  10400  uzsubsubfz  10404  fzrevral2  10465  fzshftral  10467  fz0fzdiffz0  10489  elfzmlbp  10491  elfzo  10508  nelfzo  10511  fzoaddel2  10560  fzosubel2  10565  elfzom1p1elfzo  10584  ssfzo12bi  10595  subfzo0  10613  flltdivnn0lt  10691  modqmulnn  10731  modfzo0difsn  10784  expdivap  10979  expubnd  10985  mulbinom2  11045  bernneq2  11051  ccatval1  11313  ccatval3  11315  ccatfv0  11319  ccatval1lsw  11320  ccatws1lenp1bg  11351  pfxsuffeqwrdeq  11418  pfxsuff1eqwrdeq  11419  swrdswrd  11425  pfxpfx  11428  wrd2ind  11443  swrdccatin1  11445  pfxccatin12lem1  11448  swrdccatin2  11449  pfxccatin12lem3  11452  swrdccat  11455  pfxccatpfx1  11456  pfxccatpfx2  11457  swrdccat3blem  11459  shftuz  11530  shftval2  11539  abs3dif  11819  xrmaxlesup  11973  xrltmininf  11984  xrlemininf  11985  sin02gt0  12479  dvdsval2  12505  dvdscmul  12533  dvdsmulc  12534  ndvdssub  12645  rpmulgcd  12751  cncongr1  12829  cncongr2  12830  isprm3  12844  coprimeprodsq  12984  pythagtriplem12  13002  pythagtriplem14  13004  pcmul  13028  pcdiv  13029  pcqcl  13033  pcqdiv  13034  pcdvdsb  13047  ercpbl  13599  mgmb1mgm1  13635  grpinvid1  13811  grpinvid2  13812  grpasscan1  13822  grpasscan2  13823  grpinvadd  13837  grpsubf  13838  grpsubrcan  13840  grpinvsub  13841  grpsubeq0  13845  grpsubadd0sub  13846  grppncan  13850  grpnpcan  13851  mulgnn0p1  13890  mulgaddcomlem  13902  mulginvcom  13904  mulginvinv  13905  subgsubcl  13942  subgsub  13943  eqglact  13982  quselbasg  13987  quseccl0g  13988  qussub  13994  ghmsub  14008  subcmnd  14090  rng1zrlem  14202  dvrcl  14384  unitdvcl  14385  dvrcan1  14389  dvrcan3  14390  dvreq1  14391  subrgdv  14488  lmodvsubval2  14620  lmodprop2d  14626  zndvds  14927  ntrin  15119  elnei  15147  cnrest2  15231  psmetsym  15324  psmetge0  15326  xmetge0  15360  xmetsym  15363  cnmet  15525  rpcxpsub  15903  rpdivcxp  15906  logbleb  15956  logblt  15957  lgsmodeq  16048  lgsmulsqcoprm  16049  gausslemma2dlem1a  16061  2lgsoddprmlem2  16109  upgrpredgv  16271  issubgr2  16383  uhgrissubgr  16386  egrsubgr  16388  upgrwlkvtxedg  16489  clwwlk1loop  16524  clwwlkccatlem  16525  clwwlknonex2lem2  16563  bj-peano4  16865