Theorem 3adant2 1040

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

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

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 1004

This theorem is referenced by:  3ad2ant1  1042  3imp3i2an  1207  eupickb  2159  vtoclegft  2875  eqeu  2973  ifnebibdc  3648  suc11g  4650  soinxp  4791  funopg  5355  fnco  5434  dff1o2  5582  fnimapr  5699  fvun1  5705  fvmptt  5731  fnreseql  5750  fvpr1g  5852  fvpr2g  5853  f1elima  5906  f1ocnvfvb  5913  ovexg  6044  oprssov  6156  poxp  6389  smoiso  6459  rdgivallem  6538  nndi  6645  nndir  6649  fnsnsplitdc  6664  nnaord  6668  nnaordr  6669  nnaword  6670  nnawordi  6674  ecopovtrn  6792  ecopovtrng  6795  xpdom3m  7006  mapxpen  7022  findcard  7063  fisseneq  7112  resfnfinfinss  7122  funrnfi  7125  netap  7456  2omotaplemap  7459  ltsopi  7523  addcanpig  7537  addassnqg  7585  distrnqg  7590  ltsonq  7601  ltmnqg  7604  prarloclemarch2  7622  nnanq0  7661  distrnq0  7662  distnq0r  7666  prltlu  7690  prarloclem5  7703  distrlem1prl  7785  distrlem1pru  7786  distrlem5prl  7789  distrlem5pru  7790  ltpopr  7798  ltsopr  7799  ltexprlemm  7803  ltexprlemfl  7812  ltexprlemfu  7814  lttrsr  7965  ltsosr  7967  ltasrg  7973  recexgt0sr  7976  mulextsr1lem  7983  mulextsr1  7984  axpre-mulext  8091  adddir  8153  axltwlin  8230  axlttrn  8231  ltleletr  8244  letr  8245  nnncan1  8398  npncan3  8400  pnpcan2  8402  subdi  8547  subdir  8548  reapcotr  8761  divmulap  8838  div23ap  8854  div13ap  8856  muldivdirap  8870  divsubdirap  8871  divcanap7  8884  ltmul2  9019  lemul2  9020  lemul2a  9022  lediv1  9032  ltmuldiv2  9038  lemuldiv2  9045  squeeze0  9067  nndivtr  9168  bndndx  9384  nn0n0n1ge2  9533  fnn0ind  9579  addlelt  9981  xrletr  10021  xrltne  10026  xleadd2a  10087  xleadd1  10088  xltadd2  10090  iooneg  10201  iccneg  10202  icoshft  10203  icoshftf1o  10204  zltaddlt1le  10220  fztri3or  10252  fzdcel  10253  fzen  10256  uzsubsubfz  10260  fzrevral2  10319  fzshftral  10321  fz0fzdiffz0  10343  elfzmlbp  10345  elfzo  10362  nelfzo  10365  fzoaddel2  10413  fzosubel2  10418  elfzom1p1elfzo  10437  ssfzo12bi  10448  subfzo0  10465  flltdivnn0lt  10541  modqmulnn  10581  modfzo0difsn  10634  expdivap  10829  expubnd  10835  mulbinom2  10895  bernneq2  10900  ccatval1  11150  ccatval3  11152  ccatfv0  11156  ccatval1lsw  11157  ccatws1lenp1bg  11188  pfxsuffeqwrdeq  11251  pfxsuff1eqwrdeq  11252  swrdswrd  11258  pfxpfx  11261  wrd2ind  11276  swrdccatin1  11278  pfxccatin12lem1  11281  swrdccatin2  11282  pfxccatin12lem3  11285  swrdccat  11288  pfxccatpfx1  11289  pfxccatpfx2  11290  swrdccat3blem  11292  shftuz  11349  shftval2  11358  abs3dif  11637  xrmaxlesup  11791  xrltmininf  11802  xrlemininf  11803  sin02gt0  12296  dvdsval2  12322  dvdscmul  12350  dvdsmulc  12351  ndvdssub  12462  rpmulgcd  12568  cncongr1  12646  cncongr2  12647  isprm3  12661  coprimeprodsq  12801  pythagtriplem12  12819  pythagtriplem14  12821  pcmul  12845  pcdiv  12846  pcqcl  12850  pcqdiv  12851  pcdvdsb  12864  ercpbl  13385  mgmb1mgm1  13422  grpinvid1  13606  grpinvid2  13607  grpasscan1  13617  grpasscan2  13618  grpinvadd  13632  grpsubf  13633  grpsubrcan  13635  grpinvsub  13636  grpsubeq0  13640  grpsubadd0sub  13641  grppncan  13645  grpnpcan  13646  mulgnn0p1  13691  mulgaddcomlem  13703  mulginvcom  13705  mulginvinv  13706  subgsubcl  13743  subgsub  13744  eqglact  13783  quselbasg  13788  quseccl0g  13789  qussub  13795  ghmsub  13809  subcmnd  13891  srg1zr  13971  dvrcl  14120  unitdvcl  14121  dvrcan1  14125  dvrcan3  14126  dvreq1  14127  subrgdv  14223  lmodvsubval2  14327  lmodprop2d  14333  zndvds  14634  ntrin  14819  elnei  14847  cnrest2  14931  psmetsym  15024  psmetge0  15026  xmetge0  15060  xmetsym  15063  cnmet  15225  rpcxpsub  15603  rpdivcxp  15606  logbleb  15656  logblt  15657  lgsmodeq  15745  lgsmulsqcoprm  15746  gausslemma2dlem1a  15758  2lgsoddprmlem2  15806  upgrpredgv  15965  upgrwlkvtxedg  16136  clwwlk1loop  16168  clwwlkccatlem  16169  bj-peano4  16427