Theorem 3adant2 1040

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

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

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 1004

This theorem is referenced by:  3ad2ant1  1042  3imp3i2an  1207  eupickb  2159  vtoclegft  2876  eqeu  2974  ifnebibdc  3649  suc11g  4653  soinxp  4794  funopg  5358  fnco  5437  dff1o2  5585  fnimapr  5702  fvun1  5708  fvmptt  5734  fnreseql  5753  fvpr1g  5855  fvpr2g  5856  f1elima  5909  f1ocnvfvb  5916  ovexg  6047  oprssov  6159  poxp  6392  smoiso  6463  rdgivallem  6542  nndi  6649  nndir  6653  fnsnsplitdc  6668  nnaord  6672  nnaordr  6673  nnaword  6674  nnawordi  6678  ecopovtrn  6796  ecopovtrng  6799  xpdom3m  7013  mapxpen  7029  findcard  7072  fisseneq  7121  resfnfinfinss  7132  funrnfi  7135  netap  7466  2omotaplemap  7469  ltsopi  7533  addcanpig  7547  addassnqg  7595  distrnqg  7600  ltsonq  7611  ltmnqg  7614  prarloclemarch2  7632  nnanq0  7671  distrnq0  7672  distnq0r  7676  prltlu  7700  prarloclem5  7713  distrlem1prl  7795  distrlem1pru  7796  distrlem5prl  7799  distrlem5pru  7800  ltpopr  7808  ltsopr  7809  ltexprlemm  7813  ltexprlemfl  7822  ltexprlemfu  7824  lttrsr  7975  ltsosr  7977  ltasrg  7983  recexgt0sr  7986  mulextsr1lem  7993  mulextsr1  7994  axpre-mulext  8101  adddir  8163  axltwlin  8240  axlttrn  8241  ltleletr  8254  letr  8255  nnncan1  8408  npncan3  8410  pnpcan2  8412  subdi  8557  subdir  8558  reapcotr  8771  divmulap  8848  div23ap  8864  div13ap  8866  muldivdirap  8880  divsubdirap  8881  divcanap7  8894  ltmul2  9029  lemul2  9030  lemul2a  9032  lediv1  9042  ltmuldiv2  9048  lemuldiv2  9055  squeeze0  9077  nndivtr  9178  bndndx  9394  nn0n0n1ge2  9543  fnn0ind  9589  addlelt  9996  xrletr  10036  xrltne  10041  xleadd2a  10102  xleadd1  10103  xltadd2  10105  iooneg  10216  iccneg  10217  icoshft  10218  icoshftf1o  10219  zltaddlt1le  10235  fztri3or  10267  fzdcel  10268  fzen  10271  uzsubsubfz  10275  fzrevral2  10334  fzshftral  10336  fz0fzdiffz0  10358  elfzmlbp  10360  elfzo  10377  nelfzo  10380  fzoaddel2  10428  fzosubel2  10433  elfzom1p1elfzo  10452  ssfzo12bi  10463  subfzo0  10481  flltdivnn0lt  10557  modqmulnn  10597  modfzo0difsn  10650  expdivap  10845  expubnd  10851  mulbinom2  10911  bernneq2  10916  ccatval1  11167  ccatval3  11169  ccatfv0  11173  ccatval1lsw  11174  ccatws1lenp1bg  11205  pfxsuffeqwrdeq  11272  pfxsuff1eqwrdeq  11273  swrdswrd  11279  pfxpfx  11282  wrd2ind  11297  swrdccatin1  11299  pfxccatin12lem1  11302  swrdccatin2  11303  pfxccatin12lem3  11306  swrdccat  11309  pfxccatpfx1  11310  pfxccatpfx2  11311  swrdccat3blem  11313  shftuz  11371  shftval2  11380  abs3dif  11659  xrmaxlesup  11813  xrltmininf  11824  xrlemininf  11825  sin02gt0  12318  dvdsval2  12344  dvdscmul  12372  dvdsmulc  12373  ndvdssub  12484  rpmulgcd  12590  cncongr1  12668  cncongr2  12669  isprm3  12683  coprimeprodsq  12823  pythagtriplem12  12841  pythagtriplem14  12843  pcmul  12867  pcdiv  12868  pcqcl  12872  pcqdiv  12873  pcdvdsb  12886  ercpbl  13407  mgmb1mgm1  13444  grpinvid1  13628  grpinvid2  13629  grpasscan1  13639  grpasscan2  13640  grpinvadd  13654  grpsubf  13655  grpsubrcan  13657  grpinvsub  13658  grpsubeq0  13662  grpsubadd0sub  13663  grppncan  13667  grpnpcan  13668  mulgnn0p1  13713  mulgaddcomlem  13725  mulginvcom  13727  mulginvinv  13728  subgsubcl  13765  subgsub  13766  eqglact  13805  quselbasg  13810  quseccl0g  13811  qussub  13817  ghmsub  13831  subcmnd  13913  srg1zr  13993  dvrcl  14142  unitdvcl  14143  dvrcan1  14147  dvrcan3  14148  dvreq1  14149  subrgdv  14245  lmodvsubval2  14349  lmodprop2d  14355  zndvds  14656  ntrin  14841  elnei  14869  cnrest2  14953  psmetsym  15046  psmetge0  15048  xmetge0  15082  xmetsym  15085  cnmet  15247  rpcxpsub  15625  rpdivcxp  15628  logbleb  15678  logblt  15679  lgsmodeq  15767  lgsmulsqcoprm  15768  gausslemma2dlem1a  15780  2lgsoddprmlem2  15828  upgrpredgv  15990  upgrwlkvtxedg  16175  clwwlk1loop  16208  clwwlkccatlem  16209  clwwlknonex2lem2  16247  bj-peano4  16500