Theorem 3adant2 957

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3ad2ant1  959  eupickb  2022  vtoclegft  2670  eqeu  2762  suc11g  4300  soinxp  4428  funopg  4954  fnco  5027  dff1o2  5151  fnimapr  5254  fvun1  5260  fvmptt  5283  fnreseql  5298  fvpr1g  5388  fvpr2g  5389  f1elima  5433  f1ocnvfvb  5440  ovexg  5559  oprssov  5662  poxp  5873  smoiso  5940  rdgivallem  5991  nndi  6088  nndir  6092  nnaord  6105  nnaordr  6106  nnaword  6107  nnawordi  6111  ecopovtrn  6226  ecopovtrng  6229  xpdom3m  6331  findcard  6372  funrnfi  6392  ltsopi  6510  addcanpig  6524  addassnqg  6572  distrnqg  6577  ltsonq  6588  ltmnqg  6591  prarloclemarch2  6609  nnanq0  6648  distrnq0  6649  distnq0r  6653  prltlu  6677  prarloclem5  6690  distrlem1prl  6772  distrlem1pru  6773  distrlem5prl  6776  distrlem5pru  6777  ltpopr  6785  ltsopr  6786  ltexprlemm  6790  ltexprlemfl  6799  ltexprlemfu  6801  lttrsr  6939  ltsosr  6941  ltasrg  6947  recexgt0sr  6950  mulextsr1lem  6956  mulextsr1  6957  axpre-mulext  7054  adddir  7110  axltwlin  7180  axlttrn  7181  ltleletr  7193  letr  7194  nnncan1  7344  npncan3  7346  pnpcan2  7348  subdi  7489  subdir  7490  reapcotr  7698  divmulap  7763  div23ap  7779  div13ap  7781  muldivdirap  7795  divsubdirap  7796  divcanap7  7809  ltmul2  7934  lemul2  7935  lemul2a  7937  lediv1  7947  ltmuldiv2  7953  lemuldiv2  7960  squeeze0  7982  nndivtr  8080  bndndx  8287  nn0n0n1ge2  8418  fnn0ind  8463  addlelt  8839  xrletr  8878  xrltne  8883  iooneg  9010  iccneg  9011  icoshft  9012  icoshftf1o  9013  zltaddlt1le  9028  fztri3or  9058  fzdcel  9059  fzen  9062  uzsubsubfz  9066  fzrevral2  9123  fzshftral  9125  fz0fzdiffz0  9141  elfzmlbp  9143  elfzo  9159  fzoaddel2  9202  fzosubel2  9204  elfzom1p1elfzo  9223  ssfzo12bi  9234  subfzo0  9251  flltdivnn0lt  9306  modqmulnn  9344  modfzo0difsn  9397  expdivap  9527  expubnd  9533  mulbinom2  9589  bernneq2  9594  shftuz  9705  shftval2  9714  abs3dif  9991  dvdsval2  10198  dvdscmul  10222  dvdsmulc  10223  ndvdssub  10330  rpmulgcd  10415  cncongr1  10485  cncongr2  10486  isprm3  10500  bj-peano4  10750