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  4649  soinxp  4789  funopg  5352  fnco  5431  dff1o2  5579  fnimapr  5696  fvun1  5702  fvmptt  5728  fnreseql  5747  fvpr1g  5849  fvpr2g  5850  f1elima  5903  f1ocnvfvb  5910  ovexg  6041  oprssov  6153  poxp  6384  smoiso  6454  rdgivallem  6533  nndi  6640  nndir  6644  fnsnsplitdc  6659  nnaord  6663  nnaordr  6664  nnaword  6665  nnawordi  6669  ecopovtrn  6787  ecopovtrng  6790  xpdom3m  7001  mapxpen  7017  findcard  7058  fisseneq  7104  resfnfinfinss  7114  funrnfi  7117  netap  7448  2omotaplemap  7451  ltsopi  7515  addcanpig  7529  addassnqg  7577  distrnqg  7582  ltsonq  7593  ltmnqg  7596  prarloclemarch2  7614  nnanq0  7653  distrnq0  7654  distnq0r  7658  prltlu  7682  prarloclem5  7695  distrlem1prl  7777  distrlem1pru  7778  distrlem5prl  7781  distrlem5pru  7782  ltpopr  7790  ltsopr  7791  ltexprlemm  7795  ltexprlemfl  7804  ltexprlemfu  7806  lttrsr  7957  ltsosr  7959  ltasrg  7965  recexgt0sr  7968  mulextsr1lem  7975  mulextsr1  7976  axpre-mulext  8083  adddir  8145  axltwlin  8222  axlttrn  8223  ltleletr  8236  letr  8237  nnncan1  8390  npncan3  8392  pnpcan2  8394  subdi  8539  subdir  8540  reapcotr  8753  divmulap  8830  div23ap  8846  div13ap  8848  muldivdirap  8862  divsubdirap  8863  divcanap7  8876  ltmul2  9011  lemul2  9012  lemul2a  9014  lediv1  9024  ltmuldiv2  9030  lemuldiv2  9037  squeeze0  9059  nndivtr  9160  bndndx  9376  nn0n0n1ge2  9525  fnn0ind  9571  addlelt  9972  xrletr  10012  xrltne  10017  xleadd2a  10078  xleadd1  10079  xltadd2  10081  iooneg  10192  iccneg  10193  icoshft  10194  icoshftf1o  10195  zltaddlt1le  10211  fztri3or  10243  fzdcel  10244  fzen  10247  uzsubsubfz  10251  fzrevral2  10310  fzshftral  10312  fz0fzdiffz0  10334  elfzmlbp  10336  elfzo  10353  nelfzo  10356  fzoaddel2  10404  fzosubel2  10409  elfzom1p1elfzo  10428  ssfzo12bi  10439  subfzo0  10456  flltdivnn0lt  10532  modqmulnn  10572  modfzo0difsn  10625  expdivap  10820  expubnd  10826  mulbinom2  10886  bernneq2  10891  ccatval1  11140  ccatval3  11142  ccatfv0  11146  ccatval1lsw  11147  ccatws1lenp1bg  11176  pfxsuffeqwrdeq  11238  pfxsuff1eqwrdeq  11239  swrdswrd  11245  pfxpfx  11248  wrd2ind  11263  swrdccatin1  11265  pfxccatin12lem1  11268  swrdccatin2  11269  pfxccatin12lem3  11272  swrdccat  11275  pfxccatpfx1  11276  pfxccatpfx2  11277  swrdccat3blem  11279  shftuz  11336  shftval2  11345  abs3dif  11624  xrmaxlesup  11778  xrltmininf  11789  xrlemininf  11790  sin02gt0  12283  dvdsval2  12309  dvdscmul  12337  dvdsmulc  12338  ndvdssub  12449  rpmulgcd  12555  cncongr1  12633  cncongr2  12634  isprm3  12648  coprimeprodsq  12788  pythagtriplem12  12806  pythagtriplem14  12808  pcmul  12832  pcdiv  12833  pcqcl  12837  pcqdiv  12838  pcdvdsb  12851  ercpbl  13372  mgmb1mgm1  13409  grpinvid1  13593  grpinvid2  13594  grpasscan1  13604  grpasscan2  13605  grpinvadd  13619  grpsubf  13620  grpsubrcan  13622  grpinvsub  13623  grpsubeq0  13627  grpsubadd0sub  13628  grppncan  13632  grpnpcan  13633  mulgnn0p1  13678  mulgaddcomlem  13690  mulginvcom  13692  mulginvinv  13693  subgsubcl  13730  subgsub  13731  eqglact  13770  quselbasg  13775  quseccl0g  13776  qussub  13782  ghmsub  13796  subcmnd  13878  srg1zr  13958  dvrcl  14107  unitdvcl  14108  dvrcan1  14112  dvrcan3  14113  dvreq1  14114  subrgdv  14210  lmodvsubval2  14314  lmodprop2d  14320  zndvds  14621  ntrin  14806  elnei  14834  cnrest2  14918  psmetsym  15011  psmetge0  15013  xmetge0  15047  xmetsym  15050  cnmet  15212  rpcxpsub  15590  rpdivcxp  15593  logbleb  15643  logblt  15644  lgsmodeq  15732  lgsmulsqcoprm  15733  gausslemma2dlem1a  15745  2lgsoddprmlem2  15793  upgrpredgv  15952  upgrwlkvtxedg  16085  bj-peano4  16342