Theorem 3adant2 981

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 943

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  3ad2ant1  983  eupickb  2054  vtoclegft  2727  eqeu  2821  suc11g  4430  soinxp  4567  funopg  5113  fnco  5187  dff1o2  5326  fnimapr  5433  fvun1  5439  fvmptt  5464  fnreseql  5482  fvpr1g  5578  fvpr2g  5579  f1elima  5626  f1ocnvfvb  5633  ovexg  5757  oprssov  5864  poxp  6081  smoiso  6151  rdgivallem  6230  nndi  6334  nndir  6338  fnsnsplitdc  6353  nnaord  6357  nnaordr  6358  nnaword  6359  nnawordi  6363  ecopovtrn  6478  ecopovtrng  6481  xpdom3m  6679  mapxpen  6693  findcard  6733  fisseneq  6771  resfnfinfinss  6778  funrnfi  6780  ltsopi  7070  addcanpig  7084  addassnqg  7132  distrnqg  7137  ltsonq  7148  ltmnqg  7151  prarloclemarch2  7169  nnanq0  7208  distrnq0  7209  distnq0r  7213  prltlu  7237  prarloclem5  7250  distrlem1prl  7332  distrlem1pru  7333  distrlem5prl  7336  distrlem5pru  7337  ltpopr  7345  ltsopr  7346  ltexprlemm  7350  ltexprlemfl  7359  ltexprlemfu  7361  lttrsr  7499  ltsosr  7501  ltasrg  7507  recexgt0sr  7510  mulextsr1lem  7516  mulextsr1  7517  axpre-mulext  7617  adddir  7675  axltwlin  7750  axlttrn  7751  ltleletr  7763  letr  7764  nnncan1  7915  npncan3  7917  pnpcan2  7919  subdi  8060  subdir  8061  reapcotr  8272  divmulap  8342  div23ap  8358  div13ap  8360  muldivdirap  8374  divsubdirap  8375  divcanap7  8388  ltmul2  8518  lemul2  8519  lemul2a  8521  lediv1  8531  ltmuldiv2  8537  lemuldiv2  8544  squeeze0  8566  nndivtr  8666  bndndx  8874  nn0n0n1ge2  9019  fnn0ind  9065  addlelt  9442  xrletr  9478  xrltne  9483  xleadd2a  9544  xleadd1  9545  xltadd2  9547  iooneg  9658  iccneg  9659  icoshft  9660  icoshftf1o  9661  zltaddlt1le  9676  fztri3or  9706  fzdcel  9707  fzen  9710  uzsubsubfz  9714  fzrevral2  9773  fzshftral  9775  fz0fzdiffz0  9794  elfzmlbp  9796  elfzo  9813  fzoaddel2  9857  fzosubel2  9859  elfzom1p1elfzo  9878  ssfzo12bi  9889  subfzo0  9906  flltdivnn0lt  9964  modqmulnn  10002  modfzo0difsn  10055  expdivap  10231  expubnd  10237  mulbinom2  10295  bernneq2  10300  shftuz  10476  shftval2  10485  abs3dif  10763  xrmaxlesup  10914  xrltmininf  10925  xrlemininf  10926  sin02gt0  11315  dvdsval2  11338  dvdscmul  11362  dvdsmulc  11363  ndvdssub  11469  rpmulgcd  11554  cncongr1  11624  cncongr2  11625  isprm3  11639  ntrin  12130  elnei  12158  cnrest2  12241  psmetsym  12312  psmetge0  12314  xmetge0  12348  xmetsym  12351  cnmet  12513  bj-peano4  12836