Theorem 3adant2 1042

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

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

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 1006

This theorem is referenced by:  3ad2ant1  1044  3imp3i2an  1209  eupickb  2161  vtoclegft  2878  eqeu  2976  ifnebibdc  3651  suc11g  4655  soinxp  4796  funopg  5360  fnco  5440  dff1o2  5588  fnimapr  5706  fvun1  5712  fvmptt  5738  fnreseql  5757  fvpr1g  5860  fvpr2g  5861  f1elima  5914  f1ocnvfvb  5921  ovexg  6052  oprssov  6164  poxp  6397  smoiso  6468  rdgivallem  6547  nndi  6654  nndir  6658  fnsnsplitdc  6673  nnaord  6677  nnaordr  6678  nnaword  6679  nnawordi  6683  ecopovtrn  6801  ecopovtrng  6804  xpdom3m  7018  mapxpen  7034  findcard  7077  fisseneq  7127  resfnfinfinss  7138  funrnfi  7141  netap  7473  2omotaplemap  7476  ltsopi  7540  addcanpig  7554  addassnqg  7602  distrnqg  7607  ltsonq  7618  ltmnqg  7621  prarloclemarch2  7639  nnanq0  7678  distrnq0  7679  distnq0r  7683  prltlu  7707  prarloclem5  7720  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  ltpopr  7815  ltsopr  7816  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  lttrsr  7982  ltsosr  7984  ltasrg  7990  recexgt0sr  7993  mulextsr1lem  8000  mulextsr1  8001  axpre-mulext  8108  adddir  8170  axltwlin  8247  axlttrn  8248  ltleletr  8261  letr  8262  nnncan1  8415  npncan3  8417  pnpcan2  8419  subdi  8564  subdir  8565  reapcotr  8778  divmulap  8855  div23ap  8871  div13ap  8873  muldivdirap  8887  divsubdirap  8888  divcanap7  8901  ltmul2  9036  lemul2  9037  lemul2a  9039  lediv1  9049  ltmuldiv2  9055  lemuldiv2  9062  squeeze0  9084  nndivtr  9185  bndndx  9401  nn0n0n1ge2  9550  fnn0ind  9596  addlelt  10003  xrletr  10043  xrltne  10048  xleadd2a  10109  xleadd1  10110  xltadd2  10112  iooneg  10223  iccneg  10224  icoshft  10225  icoshftf1o  10226  zltaddlt1le  10242  fztri3or  10274  fzdcel  10275  fzen  10278  uzsubsubfz  10282  fzrevral2  10341  fzshftral  10343  fz0fzdiffz0  10365  elfzmlbp  10367  elfzo  10384  nelfzo  10387  fzoaddel2  10436  fzosubel2  10441  elfzom1p1elfzo  10460  ssfzo12bi  10471  subfzo0  10489  flltdivnn0lt  10565  modqmulnn  10605  modfzo0difsn  10658  expdivap  10853  expubnd  10859  mulbinom2  10919  bernneq2  10924  ccatval1  11178  ccatval3  11180  ccatfv0  11184  ccatval1lsw  11185  ccatws1lenp1bg  11216  pfxsuffeqwrdeq  11283  pfxsuff1eqwrdeq  11284  swrdswrd  11290  pfxpfx  11293  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem3  11317  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  swrdccat3blem  11324  shftuz  11382  shftval2  11391  abs3dif  11670  xrmaxlesup  11824  xrltmininf  11835  xrlemininf  11836  sin02gt0  12330  dvdsval2  12356  dvdscmul  12384  dvdsmulc  12385  ndvdssub  12496  rpmulgcd  12602  cncongr1  12680  cncongr2  12681  isprm3  12695  coprimeprodsq  12835  pythagtriplem12  12853  pythagtriplem14  12855  pcmul  12879  pcdiv  12880  pcqcl  12884  pcqdiv  12885  pcdvdsb  12898  ercpbl  13419  mgmb1mgm1  13456  grpinvid1  13640  grpinvid2  13641  grpasscan1  13651  grpasscan2  13652  grpinvadd  13666  grpsubf  13667  grpsubrcan  13669  grpinvsub  13670  grpsubeq0  13674  grpsubadd0sub  13675  grppncan  13679  grpnpcan  13680  mulgnn0p1  13725  mulgaddcomlem  13737  mulginvcom  13739  mulginvinv  13740  subgsubcl  13777  subgsub  13778  eqglact  13817  quselbasg  13822  quseccl0g  13823  qussub  13829  ghmsub  13843  subcmnd  13925  srg1zr  14006  dvrcl  14155  unitdvcl  14156  dvrcan1  14160  dvrcan3  14161  dvreq1  14162  subrgdv  14258  lmodvsubval2  14362  lmodprop2d  14368  zndvds  14669  ntrin  14854  elnei  14882  cnrest2  14966  psmetsym  15059  psmetge0  15061  xmetge0  15095  xmetsym  15098  cnmet  15260  rpcxpsub  15638  rpdivcxp  15641  logbleb  15691  logblt  15692  lgsmodeq  15780  lgsmulsqcoprm  15781  gausslemma2dlem1a  15793  2lgsoddprmlem2  15841  upgrpredgv  16003  issubgr2  16115  uhgrissubgr  16118  egrsubgr  16120  upgrwlkvtxedg  16221  clwwlk1loop  16256  clwwlkccatlem  16257  clwwlknonex2lem2  16295  bj-peano4  16576