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  4706  soinxp  4847  funopg  5414  fnco  5494  dff1o2  5647  fnimapr  5766  fvun1  5772  fvmptt  5800  fnreseql  5822  fvpr1g  5924  fvpr2g  5925  f1elima  5982  f1ocnvfvb  5989  ovexg  6122  oprssov  6234  poxp  6472  smoiso  6577  rdgivallem  6656  nndi  6763  nndir  6767  fnsnsplitdc  6782  nnaord  6786  nnaordr  6787  nnaword  6788  nnawordi  6792  ecopovtrn  6910  ecopovtrng  6913  mapsnd  6975  xpdom3m  7137  mapxpen  7153  findcard  7197  fisseneq  7247  resfnfinfinss  7258  funrnfi  7261  netap  7627  2omotaplemap  7630  ltsopi  7694  addcanpig  7708  addassnqg  7756  distrnqg  7761  ltsonq  7772  ltmnqg  7775  prarloclemarch2  7793  nnanq0  7832  distrnq0  7833  distnq0r  7837  prltlu  7861  prarloclem5  7874  distrlem1prl  7956  distrlem1pru  7957  distrlem5prl  7960  distrlem5pru  7961  ltpopr  7969  ltsopr  7970  ltexprlemm  7974  ltexprlemfl  7983  ltexprlemfu  7985  lttrsr  8136  ltsosr  8138  ltasrg  8144  recexgt0sr  8147  mulextsr1lem  8154  mulextsr1  8155  axpre-mulext  8262  adddir  8324  axltwlin  8400  axlttrn  8401  ltleletr  8414  letr  8415  nnncan1  8570  npncan3  8572  pnpcan2  8574  subdi  8720  subdir  8721  reapcotr  8935  divmulap  9014  div23ap  9030  div13ap  9032  muldivdirap  9046  divsubdirap  9047  divcanap7  9060  ltmul2  9195  lemul2  9196  lemul2a  9198  lediv1  9208  ltmuldiv2  9214  lemuldiv2  9221  squeeze0  9243  nndivtr  9356  bndndx  9574  nn0n0n1ge2  9727  fnn0ind  9774  addlelt  10187  xrletr  10228  xrltne  10233  xleadd2a  10294  xleadd1  10295  xltadd2  10297  iooneg  10408  iccneg  10409  icoshft  10410  icoshftf1o  10411  zltaddlt1le  10428  fztri3or  10461  fzdcel  10462  fzen  10465  uzsubsubfz  10470  fzrevral2  10531  fzshftral  10533  fz0fzdiffz0  10555  elfzmlbp  10557  elfzo  10574  nelfzo  10577  fzoaddel2  10626  fzosubel2  10631  elfzom1p1elfzo  10650  ssfzo12bi  10661  subfzo0  10679  flltdivnn0lt  10761  modqmulnn  10801  modfzo0difsn  10854  expdivap  11049  expubnd  11055  mulbinom2  11115  bernneq2  11121  ccatval1  11388  ccatval3  11390  ccatfv0  11394  ccatval1lsw  11395  ccatws1lenp1bg  11426  pfxsuffeqwrdeq  11493  pfxsuff1eqwrdeq  11494  swrdswrd  11500  pfxpfx  11503  wrd2ind  11518  swrdccatin1  11520  pfxccatin12lem1  11523  swrdccatin2  11524  pfxccatin12lem3  11527  swrdccat  11530  pfxccatpfx1  11531  pfxccatpfx2  11532  swrdccat3blem  11534  shftuz  11605  shftval2  11614  abs3dif  11895  xrmaxlesup  12051  xrltmininf  12062  xrlemininf  12063  sin02gt0  12557  dvdsval2  12583  dvdscmul  12611  dvdsmulc  12612  ndvdssub  12723  rpmulgcd  12829  cncongr1  12907  cncongr2  12908  isprm3  12922  coprimeprodsq  13066  pythagtriplem12  13084  pythagtriplem14  13086  pcmul  13110  pcdiv  13111  pcqcl  13115  pcqdiv  13116  pcdvdsb  13129  ercpbl  13712  mgmb1mgm1  13748  grpinvid1  13917  grpinvid2  13918  grpasscan1  13928  grpasscan2  13929  grpinvadd  13943  grpsubf  13944  grpsubrcan  13946  grpinvsub  13947  grpsubeq0  13951  grpsubadd0sub  13952  grppncan  13956  grpnpcan  13957  mulgnn0p1  13996  mulgaddcomlem  14008  mulginvcom  14010  mulginvinv  14011  subgsubcl  14048  subgsub  14049  eqglact  14088  quselbasg  14093  quseccl0g  14094  qussub  14100  ghmsub  14114  subcmnd  14228  rng1zrlem  14366  dvrcl  14552  unitdvcl  14553  dvrcan1  14557  dvrcan3  14558  dvreq1  14559  subrgdv  14656  lmodvsubval2  14789  lmodprop2d  14795  zndvds  15094  ascldimul  15141  ntrin  15362  elnei  15390  cnrest2  15474  psmetsym  15567  psmetge0  15569  xmetge0  15603  xmetsym  15606  cnmet  15768  rpcxpsub  16153  rpdivcxp  16156  logbleb  16209  logblt  16210  lgsmodeq  16381  lgsmulsqcoprm  16382  gausslemma2dlem1a  16394  2lgsoddprmlem2  16442  upgrpredgv  16604  issubgr2  16716  uhgrissubgr  16719  egrsubgr  16721  upgrwlkvtxedg  16822  clwwlk1loop  16857  clwwlkccatlem  16858  clwwlknonex2lem2  16896  bj-peano4  17198