Theorem adantrd 393

Description: Deduction adding a conjunct to the right of an antecedent.

Hypothesis

Ref	Expression
adantrd.1	|- (ph -> (ps -> ch))

Assertion

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

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		adantrd.1	. 2 |- (ph -> (ps -> ch))
2		pm3.26 319	. 2 |- ((ps /\ th) -> ps)
3	1, 2	syl5 21	1 |- (ph -> ((ps /\ th) -> ch))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  adantrr 397  consensus 769  2eu3 1454  unineq 2258  axsep 2707  elssabg 2731  tz7.7 2979  oneqmini 3023  vtoclrbr 3218  fconst5 3854  fconstfv 3855  isomin 3905  isofrlem 3907  oecl 4178  oawordri 4190  omwordri 4209  odi 4216  unen 4440  mapenlem2 4496  pssnn 4544  brdom6disj 4815  cardinfima 4902  indpi 5046  1idpr 5145  prlem934a 5149  xrlttrt 5565  infm3 6056  infmsup 6070  supxrre 6085  uzind 6207  uzwo4OLD 6212  qbtwnre 6279  uzwo 6456  uzwoOLD 6457  sqlecant 6642  bccl2t 6971  infpnlem1 7507  ruclem13 7523  infxpidmlem8 7560  isnei 7715  metcnss 7895  metelcls 7962  iscms2lem4 7989  bcthlem16 8011  bcthlem20 8015  occllem6 9173  nmcopexlem6 9951  nmcfnexlem6 9980  cnlnssadj 10008  atexcht 10303  mdsymlem5 10329  elghomlem2 10378  mapudiscn 10498  cmpmon 10714

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain