Theorem adantrd 400

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 326	. 2 |- ((ps /\ th) -> ps)
3	1, 2	syl5 21	1 |- (ph -> ((ps /\ th) -> ch))

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  adantrr 404  jaoa 437  consensus 779  2eu3 1494  unineq 2306  axsep 2757  elssabg 2781  tz7.7 3030  oneqmini 3074  vtoclrbr 3269  fconst5 3905  fconstfv 3906  isomin 3957  isofrlem 3959  oecl 4230  oawordri 4242  omwordri 4261  odi 4268  unen 4497  mapenlem2 4555  pssnn 4599  brdom6disj 4867  cardinfima 4956  indpi 5099  1idpr 5198  prlem934a 5202  xrlttr 5618  infm3 6136  infmsup 6150  supxrre 6165  uzind 6290  uzwo4OLD 6295  qbtwnre 6331  uzwo 6481  uzwoOLD 6482  sqlecan 6730  bccl2 7061  infpnlem1 7598  ruclem13 7614  infxpidmlem8 7651  isnei 7803  metcnss 7983  metelcls 8050  iscms2lem4 8077  bcthlem16 8099  bcthlem20 8103  occllem6 9261  nmcopexlem6 10039  nmcfnexlem6 10068  cnlnssadj 10096  atexch 10392  mdsymlem5 10418  elghomlem2 10468  mapudiscn 10606  cmpmon 10825  iepiclem 10833

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 154  df-an 232

Copyright terms: Public domain