Theorem 3adant2 1018

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

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

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 982

This theorem is referenced by:  3ad2ant1  1020  3imp3i2an  1185  eupickb  2119  vtoclegft  2824  eqeu  2922  suc11g  4574  soinxp  4714  funopg  5269  fnco  5343  dff1o2  5485  fnimapr  5597  fvun1  5603  fvmptt  5628  fnreseql  5647  fvpr1g  5743  fvpr2g  5744  f1elima  5795  f1ocnvfvb  5802  ovexg  5930  oprssov  6038  poxp  6257  smoiso  6327  rdgivallem  6406  nndi  6511  nndir  6515  fnsnsplitdc  6530  nnaord  6534  nnaordr  6535  nnaword  6536  nnawordi  6540  ecopovtrn  6658  ecopovtrng  6661  xpdom3m  6860  mapxpen  6876  findcard  6916  fisseneq  6960  resfnfinfinss  6969  funrnfi  6971  netap  7283  2omotaplemap  7286  ltsopi  7349  addcanpig  7363  addassnqg  7411  distrnqg  7416  ltsonq  7427  ltmnqg  7430  prarloclemarch2  7448  nnanq0  7487  distrnq0  7488  distnq0r  7492  prltlu  7516  prarloclem5  7529  distrlem1prl  7611  distrlem1pru  7612  distrlem5prl  7615  distrlem5pru  7616  ltpopr  7624  ltsopr  7625  ltexprlemm  7629  ltexprlemfl  7638  ltexprlemfu  7640  lttrsr  7791  ltsosr  7793  ltasrg  7799  recexgt0sr  7802  mulextsr1lem  7809  mulextsr1  7810  axpre-mulext  7917  adddir  7978  axltwlin  8055  axlttrn  8056  ltleletr  8069  letr  8070  nnncan1  8223  npncan3  8225  pnpcan2  8227  subdi  8372  subdir  8373  reapcotr  8585  divmulap  8662  div23ap  8678  div13ap  8680  muldivdirap  8694  divsubdirap  8695  divcanap7  8708  ltmul2  8843  lemul2  8844  lemul2a  8846  lediv1  8856  ltmuldiv2  8862  lemuldiv2  8869  squeeze0  8891  nndivtr  8991  bndndx  9205  nn0n0n1ge2  9353  fnn0ind  9399  addlelt  9798  xrletr  9838  xrltne  9843  xleadd2a  9904  xleadd1  9905  xltadd2  9907  iooneg  10018  iccneg  10019  icoshft  10020  icoshftf1o  10021  zltaddlt1le  10037  fztri3or  10069  fzdcel  10070  fzen  10073  uzsubsubfz  10077  fzrevral2  10136  fzshftral  10138  fz0fzdiffz0  10160  elfzmlbp  10162  elfzo  10179  fzoaddel2  10223  fzosubel2  10225  elfzom1p1elfzo  10244  ssfzo12bi  10255  subfzo0  10272  flltdivnn0lt  10335  modqmulnn  10373  modfzo0difsn  10426  expdivap  10602  expubnd  10608  mulbinom2  10668  bernneq2  10673  shftuz  10858  shftval2  10867  abs3dif  11146  xrmaxlesup  11299  xrltmininf  11310  xrlemininf  11311  sin02gt0  11803  dvdsval2  11829  dvdscmul  11857  dvdsmulc  11858  ndvdssub  11967  rpmulgcd  12059  cncongr1  12135  cncongr2  12136  isprm3  12150  coprimeprodsq  12289  pythagtriplem12  12307  pythagtriplem14  12309  pcmul  12333  pcdiv  12334  pcqcl  12338  pcqdiv  12339  pcdvdsb  12352  ercpbl  12807  mgmb1mgm1  12844  grpinvid1  12996  grpinvid2  12997  grpasscan1  13007  grpasscan2  13008  grpinvadd  13022  grpsubf  13023  grpsubrcan  13025  grpinvsub  13026  grpsubeq0  13030  grpsubadd0sub  13031  grppncan  13035  grpnpcan  13036  mulgnn0p1  13073  mulgaddcomlem  13085  mulginvcom  13087  mulginvinv  13088  subgsubcl  13124  subgsub  13125  eqglact  13164  quselbasg  13169  quseccl0g  13170  qussub  13176  ghmsub  13190  subcmnd  13270  srg1zr  13341  dvrcl  13485  unitdvcl  13486  dvrcan1  13490  dvrcan3  13491  dvreq1  13492  subrgdv  13585  lmodvsubval2  13658  lmodprop2d  13664  ntrin  14084  elnei  14112  cnrest2  14196  psmetsym  14289  psmetge0  14291  xmetge0  14325  xmetsym  14328  cnmet  14490  rpcxpsub  14789  rpdivcxp  14792  logbleb  14839  logblt  14840  lgsmodeq  14907  lgsmulsqcoprm  14908  2lgsoddprmlem2  14915  bj-peano4  15168