Theorem 3adant1 597

Description: Deduction adding a conjunct to an antecedent.

Hypothesis

Ref	Expression
3adant.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
3adant1	|- ((th /\ ph /\ ps) -> ch)

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 593	. 2 |- ((th /\ ph /\ ps) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 12	1 |- ((th /\ ph /\ ps) -> ch)

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  find 2396  eloprabg 3035  oprabvalig 3048  oaord 3149  oacan 3150  nnaordr 3178  nndi 3180  nnmass 3181  nnmord 3189  nnmcan 3190  ecopoprtrn 3247  eceqopreq 3249  ltsopi 3810  genpass 3906  ltsopr 3930  adddirt 4103  add23t 4126  addsubasst 4150  mul23t 4176  subsubt 4203  ltletrt 4290  letrt 4291  ltadd2t 4349  leadd2t 4351  lesub1t 4352  ltsubadd2t 4354  lesubadd2t 4356  ledivt 4405  ltdivmult 4408  seqrn 4673  hvadd23t 5011  hvaddsub12t 5015  hvaddsubasst 5018  his5 5050  his2subt 5052  shlej1t 5356  shlej2t 5357  cvntrt 5724  atcv1 5768  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org