Theorem 3adant2 1000

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

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

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

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

This theorem is referenced by:  3ad2ant1  1002  eupickb  2080  vtoclegft  2758  eqeu  2854  suc11g  4472  soinxp  4609  funopg  5157  fnco  5231  dff1o2  5372  fnimapr  5481  fvun1  5487  fvmptt  5512  fnreseql  5530  fvpr1g  5626  fvpr2g  5627  f1elima  5674  f1ocnvfvb  5681  ovexg  5805  oprssov  5912  poxp  6129  smoiso  6199  rdgivallem  6278  nndi  6382  nndir  6386  fnsnsplitdc  6401  nnaord  6405  nnaordr  6406  nnaword  6407  nnawordi  6411  ecopovtrn  6526  ecopovtrng  6529  xpdom3m  6728  mapxpen  6742  findcard  6782  fisseneq  6820  resfnfinfinss  6828  funrnfi  6830  ltsopi  7128  addcanpig  7142  addassnqg  7190  distrnqg  7195  ltsonq  7206  ltmnqg  7209  prarloclemarch2  7227  nnanq0  7266  distrnq0  7267  distnq0r  7271  prltlu  7295  prarloclem5  7308  distrlem1prl  7390  distrlem1pru  7391  distrlem5prl  7394  distrlem5pru  7395  ltpopr  7403  ltsopr  7404  ltexprlemm  7408  ltexprlemfl  7417  ltexprlemfu  7419  lttrsr  7570  ltsosr  7572  ltasrg  7578  recexgt0sr  7581  mulextsr1lem  7588  mulextsr1  7589  axpre-mulext  7696  adddir  7757  axltwlin  7832  axlttrn  7833  ltleletr  7846  letr  7847  nnncan1  7998  npncan3  8000  pnpcan2  8002  subdi  8147  subdir  8148  reapcotr  8360  divmulap  8435  div23ap  8451  div13ap  8453  muldivdirap  8467  divsubdirap  8468  divcanap7  8481  ltmul2  8614  lemul2  8615  lemul2a  8617  lediv1  8627  ltmuldiv2  8633  lemuldiv2  8640  squeeze0  8662  nndivtr  8762  bndndx  8976  nn0n0n1ge2  9121  fnn0ind  9167  addlelt  9555  xrletr  9591  xrltne  9596  xleadd2a  9657  xleadd1  9658  xltadd2  9660  iooneg  9771  iccneg  9772  icoshft  9773  icoshftf1o  9774  zltaddlt1le  9789  fztri3or  9819  fzdcel  9820  fzen  9823  uzsubsubfz  9827  fzrevral2  9886  fzshftral  9888  fz0fzdiffz0  9907  elfzmlbp  9909  elfzo  9926  fzoaddel2  9970  fzosubel2  9972  elfzom1p1elfzo  9991  ssfzo12bi  10002  subfzo0  10019  flltdivnn0lt  10077  modqmulnn  10115  modfzo0difsn  10168  expdivap  10344  expubnd  10350  mulbinom2  10408  bernneq2  10413  shftuz  10589  shftval2  10598  abs3dif  10877  xrmaxlesup  11028  xrltmininf  11039  xrlemininf  11040  sin02gt0  11470  dvdsval2  11496  dvdscmul  11520  dvdsmulc  11521  ndvdssub  11627  rpmulgcd  11714  cncongr1  11784  cncongr2  11785  isprm3  11799  ntrin  12293  elnei  12321  cnrest2  12405  psmetsym  12498  psmetge0  12500  xmetge0  12534  xmetsym  12537  cnmet  12699  bj-peano4  13153