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  2875  eqeu  2973  ifnebibdc  3648  suc11g  4646  soinxp  4786  funopg  5348  fnco  5427  dff1o2  5573  fnimapr  5687  fvun1  5693  fvmptt  5719  fnreseql  5738  fvpr1g  5838  fvpr2g  5839  f1elima  5890  f1ocnvfvb  5897  ovexg  6028  oprssov  6138  poxp  6368  smoiso  6438  rdgivallem  6517  nndi  6622  nndir  6626  fnsnsplitdc  6641  nnaord  6645  nnaordr  6646  nnaword  6647  nnawordi  6651  ecopovtrn  6769  ecopovtrng  6772  xpdom3m  6981  mapxpen  6997  findcard  7038  fisseneq  7084  resfnfinfinss  7094  funrnfi  7097  netap  7428  2omotaplemap  7431  ltsopi  7495  addcanpig  7509  addassnqg  7557  distrnqg  7562  ltsonq  7573  ltmnqg  7576  prarloclemarch2  7594  nnanq0  7633  distrnq0  7634  distnq0r  7638  prltlu  7662  prarloclem5  7675  distrlem1prl  7757  distrlem1pru  7758  distrlem5prl  7761  distrlem5pru  7762  ltpopr  7770  ltsopr  7771  ltexprlemm  7775  ltexprlemfl  7784  ltexprlemfu  7786  lttrsr  7937  ltsosr  7939  ltasrg  7945  recexgt0sr  7948  mulextsr1lem  7955  mulextsr1  7956  axpre-mulext  8063  adddir  8125  axltwlin  8202  axlttrn  8203  ltleletr  8216  letr  8217  nnncan1  8370  npncan3  8372  pnpcan2  8374  subdi  8519  subdir  8520  reapcotr  8733  divmulap  8810  div23ap  8826  div13ap  8828  muldivdirap  8842  divsubdirap  8843  divcanap7  8856  ltmul2  8991  lemul2  8992  lemul2a  8994  lediv1  9004  ltmuldiv2  9010  lemuldiv2  9017  squeeze0  9039  nndivtr  9140  bndndx  9356  nn0n0n1ge2  9505  fnn0ind  9551  addlelt  9952  xrletr  9992  xrltne  9997  xleadd2a  10058  xleadd1  10059  xltadd2  10061  iooneg  10172  iccneg  10173  icoshft  10174  icoshftf1o  10175  zltaddlt1le  10191  fztri3or  10223  fzdcel  10224  fzen  10227  uzsubsubfz  10231  fzrevral2  10290  fzshftral  10292  fz0fzdiffz0  10314  elfzmlbp  10316  elfzo  10333  nelfzo  10336  fzoaddel2  10383  fzosubel2  10388  elfzom1p1elfzo  10407  ssfzo12bi  10418  subfzo0  10435  flltdivnn0lt  10511  modqmulnn  10551  modfzo0difsn  10604  expdivap  10799  expubnd  10805  mulbinom2  10865  bernneq2  10870  ccatval1  11118  ccatval3  11120  ccatfv0  11124  ccatval1lsw  11125  ccatws1lenp1bg  11154  pfxsuffeqwrdeq  11216  pfxsuff1eqwrdeq  11217  swrdswrd  11223  pfxpfx  11226  wrd2ind  11241  swrdccatin1  11243  pfxccatin12lem1  11246  swrdccatin2  11247  pfxccatin12lem3  11250  swrdccat  11253  pfxccatpfx1  11254  pfxccatpfx2  11255  swrdccat3blem  11257  shftuz  11314  shftval2  11323  abs3dif  11602  xrmaxlesup  11756  xrltmininf  11767  xrlemininf  11768  sin02gt0  12261  dvdsval2  12287  dvdscmul  12315  dvdsmulc  12316  ndvdssub  12427  rpmulgcd  12533  cncongr1  12611  cncongr2  12612  isprm3  12626  coprimeprodsq  12766  pythagtriplem12  12784  pythagtriplem14  12786  pcmul  12810  pcdiv  12811  pcqcl  12815  pcqdiv  12816  pcdvdsb  12829  ercpbl  13350  mgmb1mgm1  13387  grpinvid1  13571  grpinvid2  13572  grpasscan1  13582  grpasscan2  13583  grpinvadd  13597  grpsubf  13598  grpsubrcan  13600  grpinvsub  13601  grpsubeq0  13605  grpsubadd0sub  13606  grppncan  13610  grpnpcan  13611  mulgnn0p1  13656  mulgaddcomlem  13668  mulginvcom  13670  mulginvinv  13671  subgsubcl  13708  subgsub  13709  eqglact  13748  quselbasg  13753  quseccl0g  13754  qussub  13760  ghmsub  13774  subcmnd  13856  srg1zr  13936  dvrcl  14084  unitdvcl  14085  dvrcan1  14089  dvrcan3  14090  dvreq1  14091  subrgdv  14187  lmodvsubval2  14291  lmodprop2d  14297  zndvds  14598  ntrin  14783  elnei  14811  cnrest2  14895  psmetsym  14988  psmetge0  14990  xmetge0  15024  xmetsym  15027  cnmet  15189  rpcxpsub  15567  rpdivcxp  15570  logbleb  15620  logblt  15621  lgsmodeq  15709  lgsmulsqcoprm  15710  gausslemma2dlem1a  15722  2lgsoddprmlem2  15770  upgrpredgv  15929  bj-peano4  16248