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  2126  vtoclegft  2836  eqeu  2934  ifnebibdc  3605  suc11g  4594  soinxp  4734  funopg  5293  fnco  5369  dff1o2  5512  fnimapr  5624  fvun1  5630  fvmptt  5656  fnreseql  5675  fvpr1g  5771  fvpr2g  5772  f1elima  5823  f1ocnvfvb  5830  ovexg  5959  oprssov  6069  poxp  6299  smoiso  6369  rdgivallem  6448  nndi  6553  nndir  6557  fnsnsplitdc  6572  nnaord  6576  nnaordr  6577  nnaword  6578  nnawordi  6582  ecopovtrn  6700  ecopovtrng  6703  xpdom3m  6902  mapxpen  6918  findcard  6958  fisseneq  7004  resfnfinfinss  7014  funrnfi  7017  netap  7337  2omotaplemap  7340  ltsopi  7404  addcanpig  7418  addassnqg  7466  distrnqg  7471  ltsonq  7482  ltmnqg  7485  prarloclemarch2  7503  nnanq0  7542  distrnq0  7543  distnq0r  7547  prltlu  7571  prarloclem5  7584  distrlem1prl  7666  distrlem1pru  7667  distrlem5prl  7670  distrlem5pru  7671  ltpopr  7679  ltsopr  7680  ltexprlemm  7684  ltexprlemfl  7693  ltexprlemfu  7695  lttrsr  7846  ltsosr  7848  ltasrg  7854  recexgt0sr  7857  mulextsr1lem  7864  mulextsr1  7865  axpre-mulext  7972  adddir  8034  axltwlin  8111  axlttrn  8112  ltleletr  8125  letr  8126  nnncan1  8279  npncan3  8281  pnpcan2  8283  subdi  8428  subdir  8429  reapcotr  8642  divmulap  8719  div23ap  8735  div13ap  8737  muldivdirap  8751  divsubdirap  8752  divcanap7  8765  ltmul2  8900  lemul2  8901  lemul2a  8903  lediv1  8913  ltmuldiv2  8919  lemuldiv2  8926  squeeze0  8948  nndivtr  9049  bndndx  9265  nn0n0n1ge2  9413  fnn0ind  9459  addlelt  9860  xrletr  9900  xrltne  9905  xleadd2a  9966  xleadd1  9967  xltadd2  9969  iooneg  10080  iccneg  10081  icoshft  10082  icoshftf1o  10083  zltaddlt1le  10099  fztri3or  10131  fzdcel  10132  fzen  10135  uzsubsubfz  10139  fzrevral2  10198  fzshftral  10200  fz0fzdiffz0  10222  elfzmlbp  10224  elfzo  10241  nelfzo  10244  fzoaddel2  10286  fzosubel2  10288  elfzom1p1elfzo  10307  ssfzo12bi  10318  subfzo0  10335  flltdivnn0lt  10411  modqmulnn  10451  modfzo0difsn  10504  expdivap  10699  expubnd  10705  mulbinom2  10765  bernneq2  10770  shftuz  10999  shftval2  11008  abs3dif  11287  xrmaxlesup  11441  xrltmininf  11452  xrlemininf  11453  sin02gt0  11946  dvdsval2  11972  dvdscmul  12000  dvdsmulc  12001  ndvdssub  12112  rpmulgcd  12218  cncongr1  12296  cncongr2  12297  isprm3  12311  coprimeprodsq  12451  pythagtriplem12  12469  pythagtriplem14  12471  pcmul  12495  pcdiv  12496  pcqcl  12500  pcqdiv  12501  pcdvdsb  12514  ercpbl  13033  mgmb1mgm1  13070  grpinvid1  13254  grpinvid2  13255  grpasscan1  13265  grpasscan2  13266  grpinvadd  13280  grpsubf  13281  grpsubrcan  13283  grpinvsub  13284  grpsubeq0  13288  grpsubadd0sub  13289  grppncan  13293  grpnpcan  13294  mulgnn0p1  13339  mulgaddcomlem  13351  mulginvcom  13353  mulginvinv  13354  subgsubcl  13391  subgsub  13392  eqglact  13431  quselbasg  13436  quseccl0g  13437  qussub  13443  ghmsub  13457  subcmnd  13539  srg1zr  13619  dvrcl  13767  unitdvcl  13768  dvrcan1  13772  dvrcan3  13773  dvreq1  13774  subrgdv  13870  lmodvsubval2  13974  lmodprop2d  13980  zndvds  14281  ntrin  14444  elnei  14472  cnrest2  14556  psmetsym  14649  psmetge0  14651  xmetge0  14685  xmetsym  14688  cnmet  14850  rpcxpsub  15228  rpdivcxp  15231  logbleb  15281  logblt  15282  lgsmodeq  15370  lgsmulsqcoprm  15371  gausslemma2dlem1a  15383  2lgsoddprmlem2  15431  bj-peano4  15685