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  6578  rdgivallem  6657  nndi  6764  nndir  6768  fnsnsplitdc  6783  nnaord  6787  nnaordr  6788  nnaword  6789  nnawordi  6793  ecopovtrn  6911  ecopovtrng  6914  mapsnd  6976  xpdom3m  7138  mapxpen  7154  findcard  7198  fisseneq  7248  resfnfinfinss  7259  funrnfi  7262  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  9725  fnn0ind  9773  addlelt  10186  xrletr  10227  xrltne  10232  xleadd2a  10293  xleadd1  10294  xltadd2  10296  iooneg  10407  iccneg  10408  icoshft  10409  icoshftf1o  10410  zltaddlt1le  10427  fztri3or  10460  fzdcel  10461  fzen  10464  uzsubsubfz  10469  fzrevral2  10530  fzshftral  10532  fz0fzdiffz0  10554  elfzmlbp  10556  elfzo  10573  nelfzo  10576  fzoaddel2  10625  fzosubel2  10630  elfzom1p1elfzo  10649  ssfzo12bi  10660  subfzo0  10678  flltdivnn0lt  10760  modqmulnn  10800  modfzo0difsn  10853  expdivap  11048  expubnd  11054  mulbinom2  11114  bernneq2  11120  ccatval1  11387  ccatval3  11389  ccatfv0  11393  ccatval1lsw  11394  ccatws1lenp1bg  11425  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  swrdswrd  11499  pfxpfx  11502  wrd2ind  11517  swrdccatin1  11519  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem3  11526  swrdccat  11529  pfxccatpfx1  11530  pfxccatpfx2  11531  swrdccat3blem  11533  shftuz  11604  shftval2  11613  abs3dif  11894  xrmaxlesup  12050  xrltmininf  12061  xrlemininf  12062  sin02gt0  12556  dvdsval2  12582  dvdscmul  12610  dvdsmulc  12611  ndvdssub  12722  rpmulgcd  12828  cncongr1  12906  cncongr2  12907  isprm3  12921  coprimeprodsq  13065  pythagtriplem12  13083  pythagtriplem14  13085  pcmul  13109  pcdiv  13110  pcqcl  13114  pcqdiv  13115  pcdvdsb  13128  ercpbl  13711  mgmb1mgm1  13747  grpinvid1  13916  grpinvid2  13917  grpasscan1  13927  grpasscan2  13928  grpinvadd  13942  grpsubf  13943  grpsubrcan  13945  grpinvsub  13946  grpsubeq0  13950  grpsubadd0sub  13951  grppncan  13955  grpnpcan  13956  mulgnn0p1  13995  mulgaddcomlem  14007  mulginvcom  14009  mulginvinv  14010  subgsubcl  14047  subgsub  14048  eqglact  14087  quselbasg  14092  quseccl0g  14093  qussub  14099  ghmsub  14113  subcmnd  14227  rng1zrlem  14365  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  dvreq1  14558  subrgdv  14655  lmodvsubval2  14788  lmodprop2d  14794  zndvds  15093  ascldimul  15140  ntrin  15383  elnei  15411  cnrest2  15495  psmetsym  15588  psmetge0  15590  xmetge0  15624  xmetsym  15627  cnmet  15789  rpcxpsub  16174  rpdivcxp  16177  logbleb  16230  logblt  16231  lgsmodeq  16402  lgsmulsqcoprm  16403  gausslemma2dlem1a  16415  2lgsoddprmlem2  16463  upgrpredgv  16625  issubgr2  16737  uhgrissubgr  16740  egrsubgr  16742  upgrwlkvtxedg  16843  clwwlk1loop  16878  clwwlkccatlem  16879  clwwlknonex2lem2  16917  bj-peano4  17219