Theorem 3adant2 1016

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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 980

This theorem is referenced by:  3ad2ant1  1018  3imp3i2an  1183  eupickb  2105  vtoclegft  2807  eqeu  2905  suc11g  4550  soinxp  4690  funopg  5242  fnco  5316  dff1o2  5458  fnimapr  5568  fvun1  5574  fvmptt  5599  fnreseql  5618  fvpr1g  5714  fvpr2g  5715  f1elima  5764  f1ocnvfvb  5771  ovexg  5899  oprssov  6006  poxp  6223  smoiso  6293  rdgivallem  6372  nndi  6477  nndir  6481  fnsnsplitdc  6496  nnaord  6500  nnaordr  6501  nnaword  6502  nnawordi  6506  ecopovtrn  6622  ecopovtrng  6625  xpdom3m  6824  mapxpen  6838  findcard  6878  fisseneq  6921  resfnfinfinss  6929  funrnfi  6931  ltsopi  7294  addcanpig  7308  addassnqg  7356  distrnqg  7361  ltsonq  7372  ltmnqg  7375  prarloclemarch2  7393  nnanq0  7432  distrnq0  7433  distnq0r  7437  prltlu  7461  prarloclem5  7474  distrlem1prl  7556  distrlem1pru  7557  distrlem5prl  7560  distrlem5pru  7561  ltpopr  7569  ltsopr  7570  ltexprlemm  7574  ltexprlemfl  7583  ltexprlemfu  7585  lttrsr  7736  ltsosr  7738  ltasrg  7744  recexgt0sr  7747  mulextsr1lem  7754  mulextsr1  7755  axpre-mulext  7862  adddir  7923  axltwlin  7999  axlttrn  8000  ltleletr  8013  letr  8014  nnncan1  8167  npncan3  8169  pnpcan2  8171  subdi  8316  subdir  8317  reapcotr  8529  divmulap  8605  div23ap  8621  div13ap  8623  muldivdirap  8637  divsubdirap  8638  divcanap7  8651  ltmul2  8786  lemul2  8787  lemul2a  8789  lediv1  8799  ltmuldiv2  8805  lemuldiv2  8812  squeeze0  8834  nndivtr  8934  bndndx  9148  nn0n0n1ge2  9296  fnn0ind  9342  addlelt  9739  xrletr  9779  xrltne  9784  xleadd2a  9845  xleadd1  9846  xltadd2  9848  iooneg  9959  iccneg  9960  icoshft  9961  icoshftf1o  9962  zltaddlt1le  9978  fztri3or  10009  fzdcel  10010  fzen  10013  uzsubsubfz  10017  fzrevral2  10076  fzshftral  10078  fz0fzdiffz0  10100  elfzmlbp  10102  elfzo  10119  fzoaddel2  10163  fzosubel2  10165  elfzom1p1elfzo  10184  ssfzo12bi  10195  subfzo0  10212  flltdivnn0lt  10274  modqmulnn  10312  modfzo0difsn  10365  expdivap  10541  expubnd  10547  mulbinom2  10606  bernneq2  10611  shftuz  10794  shftval2  10803  abs3dif  11082  xrmaxlesup  11235  xrltmininf  11246  xrlemininf  11247  sin02gt0  11739  dvdsval2  11765  dvdscmul  11793  dvdsmulc  11794  ndvdssub  11902  rpmulgcd  11994  cncongr1  12070  cncongr2  12071  isprm3  12085  coprimeprodsq  12224  pythagtriplem12  12242  pythagtriplem14  12244  pcmul  12268  pcdiv  12269  pcqcl  12273  pcqdiv  12274  pcdvdsb  12286  mgmb1mgm1  12662  grpinvid1  12795  grpinvid2  12796  grpasscan1  12803  grpasscan2  12804  grpinvadd  12818  grpsubf  12819  grpsubrcan  12821  grpinvsub  12822  grpsubeq0  12826  grpsubadd0sub  12827  grppncan  12831  grpnpcan  12832  mulgnn0p1  12864  mulgaddcomlem  12875  mulginvcom  12877  mulginvinv  12878  srg1zr  12976  ntrin  13204  elnei  13232  cnrest2  13316  psmetsym  13409  psmetge0  13411  xmetge0  13445  xmetsym  13448  cnmet  13610  rpcxpsub  13909  rpdivcxp  13912  logbleb  13959  logblt  13960  lgsmodeq  14026  lgsmulsqcoprm  14027  bj-peano4  14276