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  7620  2omotaplemap  7623  ltsopi  7687  addcanpig  7701  addassnqg  7749  distrnqg  7754  ltsonq  7765  ltmnqg  7768  prarloclemarch2  7786  nnanq0  7825  distrnq0  7826  distnq0r  7830  prltlu  7854  prarloclem5  7867  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulextsr1lem  8147  mulextsr1  8148  axpre-mulext  8255  adddir  8317  axltwlin  8393  axlttrn  8394  ltleletr  8407  letr  8408  nnncan1  8562  npncan3  8564  pnpcan2  8566  subdi  8712  subdir  8713  reapcotr  8927  divmulap  9006  div23ap  9022  div13ap  9024  muldivdirap  9038  divsubdirap  9039  divcanap7  9052  ltmul2  9187  lemul2  9188  lemul2a  9190  lediv1  9200  ltmuldiv2  9206  lemuldiv2  9213  squeeze0  9235  nndivtr  9347  bndndx  9564  nn0n0n1ge2  9717  fnn0ind  9764  addlelt  10171  xrletr  10212  xrltne  10217  xleadd2a  10278  xleadd1  10279  xltadd2  10281  iooneg  10392  iccneg  10393  icoshft  10394  icoshftf1o  10395  zltaddlt1le  10412  fztri3or  10445  fzdcel  10446  fzen  10449  uzsubsubfz  10454  fzrevral2  10515  fzshftral  10517  fz0fzdiffz0  10539  elfzmlbp  10541  elfzo  10558  nelfzo  10561  fzoaddel2  10610  fzosubel2  10615  elfzom1p1elfzo  10634  ssfzo12bi  10645  subfzo0  10663  flltdivnn0lt  10741  modqmulnn  10781  modfzo0difsn  10834  expdivap  11029  expubnd  11035  mulbinom2  11095  bernneq2  11101  ccatval1  11367  ccatval3  11369  ccatfv0  11373  ccatval1lsw  11374  ccatws1lenp1bg  11405  pfxsuffeqwrdeq  11472  pfxsuff1eqwrdeq  11473  swrdswrd  11479  pfxpfx  11482  wrd2ind  11497  swrdccatin1  11499  pfxccatin12lem1  11502  swrdccatin2  11503  pfxccatin12lem3  11506  swrdccat  11509  pfxccatpfx1  11510  pfxccatpfx2  11511  swrdccat3blem  11513  shftuz  11584  shftval2  11593  abs3dif  11873  xrmaxlesup  12027  xrltmininf  12038  xrlemininf  12039  sin02gt0  12533  dvdsval2  12559  dvdscmul  12587  dvdsmulc  12588  ndvdssub  12699  rpmulgcd  12805  cncongr1  12883  cncongr2  12884  isprm3  12898  coprimeprodsq  13038  pythagtriplem12  13056  pythagtriplem14  13058  pcmul  13082  pcdiv  13083  pcqcl  13087  pcqdiv  13088  pcdvdsb  13101  ercpbl  13654  mgmb1mgm1  13690  grpinvid1  13859  grpinvid2  13860  grpasscan1  13870  grpasscan2  13871  grpinvadd  13885  grpsubf  13886  grpsubrcan  13888  grpinvsub  13889  grpsubeq0  13893  grpsubadd0sub  13894  grppncan  13898  grpnpcan  13899  mulgnn0p1  13938  mulgaddcomlem  13950  mulginvcom  13952  mulginvinv  13953  subgsubcl  13990  subgsub  13991  eqglact  14030  quselbasg  14035  quseccl0g  14036  qussub  14042  ghmsub  14056  subcmnd  14139  rng1zrlem  14260  dvrcl  14444  unitdvcl  14445  dvrcan1  14449  dvrcan3  14450  dvreq1  14451  subrgdv  14548  lmodvsubval2  14681  lmodprop2d  14687  zndvds  14986  ascldimul  15033  ntrin  15227  elnei  15255  cnrest2  15339  psmetsym  15432  psmetge0  15434  xmetge0  15468  xmetsym  15471  cnmet  15633  rpcxpsub  16016  rpdivcxp  16019  logbleb  16069  logblt  16070  lgsmodeq  16176  lgsmulsqcoprm  16177  gausslemma2dlem1a  16189  2lgsoddprmlem2  16237  upgrpredgv  16399  issubgr2  16511  uhgrissubgr  16514  egrsubgr  16516  upgrwlkvtxedg  16617  clwwlk1loop  16652  clwwlkccatlem  16653  clwwlknonex2lem2  16691  bj-peano4  16993