Theorem 3adant2 1047

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant1  1049  3imp3i2an  1214  eupickb  2168  vtoclegft  2897  eqeu  2996  ifnebibdc  3686  suc11g  4704  soinxp  4845  funopg  5411  fnco  5491  dff1o2  5644  fnimapr  5763  fvun1  5769  fvmptt  5797  fnreseql  5819  fvpr1g  5921  fvpr2g  5922  f1elima  5979  f1ocnvfvb  5986  ovexg  6119  oprssov  6231  poxp  6468  smoiso  6573  rdgivallem  6652  nndi  6759  nndir  6763  fnsnsplitdc  6778  nnaord  6782  nnaordr  6783  nnaword  6784  nnawordi  6788  ecopovtrn  6906  ecopovtrng  6909  mapsnd  6970  xpdom3m  7132  mapxpen  7148  findcard  7192  fisseneq  7242  resfnfinfinss  7253  funrnfi  7256  netap  7621  2omotaplemap  7624  ltsopi  7688  addcanpig  7702  addassnqg  7750  distrnqg  7755  ltsonq  7766  ltmnqg  7769  prarloclemarch2  7787  nnanq0  7826  distrnq0  7827  distnq0r  7831  prltlu  7855  prarloclem5  7868  distrlem1prl  7950  distrlem1pru  7951  distrlem5prl  7954  distrlem5pru  7955  ltpopr  7963  ltsopr  7964  ltexprlemm  7968  ltexprlemfl  7977  ltexprlemfu  7979  lttrsr  8130  ltsosr  8132  ltasrg  8138  recexgt0sr  8141  mulextsr1lem  8148  mulextsr1  8149  axpre-mulext  8256  adddir  8318  axltwlin  8394  axlttrn  8395  ltleletr  8408  letr  8409  nnncan1  8564  npncan3  8566  pnpcan2  8568  subdi  8714  subdir  8715  reapcotr  8929  divmulap  9008  div23ap  9024  div13ap  9026  muldivdirap  9040  divsubdirap  9041  divcanap7  9054  ltmul2  9189  lemul2  9190  lemul2a  9192  lediv1  9202  ltmuldiv2  9208  lemuldiv2  9215  squeeze0  9237  nndivtr  9349  bndndx  9567  nn0n0n1ge2  9720  fnn0ind  9767  addlelt  10180  xrletr  10221  xrltne  10226  xleadd2a  10287  xleadd1  10288  xltadd2  10290  iooneg  10401  iccneg  10402  icoshft  10403  icoshftf1o  10404  zltaddlt1le  10421  fztri3or  10454  fzdcel  10455  fzen  10458  uzsubsubfz  10463  fzrevral2  10524  fzshftral  10526  fz0fzdiffz0  10548  elfzmlbp  10550  elfzo  10567  nelfzo  10570  fzoaddel2  10619  fzosubel2  10624  elfzom1p1elfzo  10643  ssfzo12bi  10654  subfzo0  10672  flltdivnn0lt  10753  modqmulnn  10793  modfzo0difsn  10846  expdivap  11041  expubnd  11047  mulbinom2  11107  bernneq2  11113  ccatval1  11380  ccatval3  11382  ccatfv0  11386  ccatval1lsw  11387  ccatws1lenp1bg  11418  pfxsuffeqwrdeq  11485  pfxsuff1eqwrdeq  11486  swrdswrd  11492  pfxpfx  11495  wrd2ind  11510  swrdccatin1  11512  pfxccatin12lem1  11515  swrdccatin2  11516  pfxccatin12lem3  11519  swrdccat  11522  pfxccatpfx1  11523  pfxccatpfx2  11524  swrdccat3blem  11526  shftuz  11597  shftval2  11606  abs3dif  11887  xrmaxlesup  12043  xrltmininf  12054  xrlemininf  12055  sin02gt0  12549  dvdsval2  12575  dvdscmul  12603  dvdsmulc  12604  ndvdssub  12715  rpmulgcd  12821  cncongr1  12899  cncongr2  12900  isprm3  12914  coprimeprodsq  13058  pythagtriplem12  13076  pythagtriplem14  13078  pcmul  13102  pcdiv  13103  pcqcl  13107  pcqdiv  13108  pcdvdsb  13121  ercpbl  13703  mgmb1mgm1  13739  grpinvid1  13908  grpinvid2  13909  grpasscan1  13919  grpasscan2  13920  grpinvadd  13934  grpsubf  13935  grpsubrcan  13937  grpinvsub  13938  grpsubeq0  13942  grpsubadd0sub  13943  grppncan  13947  grpnpcan  13948  mulgnn0p1  13987  mulgaddcomlem  13999  mulginvcom  14001  mulginvinv  14002  subgsubcl  14039  subgsub  14040  eqglact  14079  quselbasg  14084  quseccl0g  14085  qussub  14091  ghmsub  14105  subcmnd  14188  rng1zrlem  14309  dvrcl  14493  unitdvcl  14494  dvrcan1  14498  dvrcan3  14499  dvreq1  14500  subrgdv  14597  lmodvsubval2  14730  lmodprop2d  14736  zndvds  15035  ascldimul  15082  ntrin  15277  elnei  15305  cnrest2  15389  psmetsym  15482  psmetge0  15484  xmetge0  15518  xmetsym  15521  cnmet  15683  rpcxpsub  16066  rpdivcxp  16069  logbleb  16119  logblt  16120  lgsmodeq  16286  lgsmulsqcoprm  16287  gausslemma2dlem1a  16299  2lgsoddprmlem2  16347  upgrpredgv  16509  issubgr2  16621  uhgrissubgr  16624  egrsubgr  16626  upgrwlkvtxedg  16727  clwwlk1loop  16762  clwwlkccatlem  16763  clwwlknonex2lem2  16801  bj-peano4  17103