Theorem 3adant2 1006

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

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

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 970

This theorem is referenced by:  3ad2ant1  1008  3imp3i2an  1173  eupickb  2095  vtoclegft  2798  eqeu  2896  suc11g  4534  soinxp  4674  funopg  5222  fnco  5296  dff1o2  5437  fnimapr  5546  fvun1  5552  fvmptt  5577  fnreseql  5595  fvpr1g  5691  fvpr2g  5692  f1elima  5741  f1ocnvfvb  5748  ovexg  5876  oprssov  5983  poxp  6200  smoiso  6270  rdgivallem  6349  nndi  6454  nndir  6458  fnsnsplitdc  6473  nnaord  6477  nnaordr  6478  nnaword  6479  nnawordi  6483  ecopovtrn  6598  ecopovtrng  6601  xpdom3m  6800  mapxpen  6814  findcard  6854  fisseneq  6897  resfnfinfinss  6905  funrnfi  6907  ltsopi  7261  addcanpig  7275  addassnqg  7323  distrnqg  7328  ltsonq  7339  ltmnqg  7342  prarloclemarch2  7360  nnanq0  7399  distrnq0  7400  distnq0r  7404  prltlu  7428  prarloclem5  7441  distrlem1prl  7523  distrlem1pru  7524  distrlem5prl  7527  distrlem5pru  7528  ltpopr  7536  ltsopr  7537  ltexprlemm  7541  ltexprlemfl  7550  ltexprlemfu  7552  lttrsr  7703  ltsosr  7705  ltasrg  7711  recexgt0sr  7714  mulextsr1lem  7721  mulextsr1  7722  axpre-mulext  7829  adddir  7890  axltwlin  7966  axlttrn  7967  ltleletr  7980  letr  7981  nnncan1  8134  npncan3  8136  pnpcan2  8138  subdi  8283  subdir  8284  reapcotr  8496  divmulap  8571  div23ap  8587  div13ap  8589  muldivdirap  8603  divsubdirap  8604  divcanap7  8617  ltmul2  8751  lemul2  8752  lemul2a  8754  lediv1  8764  ltmuldiv2  8770  lemuldiv2  8777  squeeze0  8799  nndivtr  8899  bndndx  9113  nn0n0n1ge2  9261  fnn0ind  9307  addlelt  9704  xrletr  9744  xrltne  9749  xleadd2a  9810  xleadd1  9811  xltadd2  9813  iooneg  9924  iccneg  9925  icoshft  9926  icoshftf1o  9927  zltaddlt1le  9943  fztri3or  9974  fzdcel  9975  fzen  9978  uzsubsubfz  9982  fzrevral2  10041  fzshftral  10043  fz0fzdiffz0  10065  elfzmlbp  10067  elfzo  10084  fzoaddel2  10128  fzosubel2  10130  elfzom1p1elfzo  10149  ssfzo12bi  10160  subfzo0  10177  flltdivnn0lt  10239  modqmulnn  10277  modfzo0difsn  10330  expdivap  10506  expubnd  10512  mulbinom2  10571  bernneq2  10576  shftuz  10759  shftval2  10768  abs3dif  11047  xrmaxlesup  11200  xrltmininf  11211  xrlemininf  11212  sin02gt0  11704  dvdsval2  11730  dvdscmul  11758  dvdsmulc  11759  ndvdssub  11867  rpmulgcd  11959  cncongr1  12035  cncongr2  12036  isprm3  12050  coprimeprodsq  12189  pythagtriplem12  12207  pythagtriplem14  12209  pcmul  12233  pcdiv  12234  pcqcl  12238  pcqdiv  12239  pcdvdsb  12251  mgmb1mgm1  12599  ntrin  12764  elnei  12792  cnrest2  12876  psmetsym  12969  psmetge0  12971  xmetge0  13005  xmetsym  13008  cnmet  13170  rpcxpsub  13469  rpdivcxp  13472  logbleb  13519  logblt  13520  lgsmodeq  13586  lgsmulsqcoprm  13587  bj-peano4  13837