Theorem adantrd 391

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 395  consensus 766  2eu3 1449  unineq 2251  axsep 2697  elssabg 2721  tz7.7 2968  oneqmini 3012  vtoclrbr 3207  fconst5 3839  fconstfv 3840  isomin 3890  isofrlem 3892  oecl 4162  oawordri 4174  omwordri 4193  odi 4200  unen 4420  mapenlem2 4476  pssnn 4519  brdom6disj 4785  cardinfima 4871  indpi 5014  1idpr 5113  prlem934a 5117  xrlttrt 5534  infm3 6009  infmsup 6023  supxrre 6038  uzind 6161  uzwo4OLD 6166  qbtwnre 6224  uzwo 6395  uzwoOLD 6396  sqlecant 6580  bccl2t 6917  infpnlem1 7457  ruclem13 7473  infxpidmlem8 7510  isnei 7668  metcnss 7850  metelcls 7916  iscms2lem4 7942  bcthlem16 7964  bcthlem20 7968  occllem6 9117  nmcopexlem6 9894  nmcfnexlem6 9923  cnlnssadj 9951  atexcht 10245  mdsymlem5 10271  elghomlem2 10317  mapudiscn 10435  cmpmon 10621

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