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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  adantrr 395  jaoa 428  consensus 772  2eu3 1491  unineq 2307  axsep 2776  elssabg 2800  tz7.7 3001  oneqmini 3024  suctr 3055  vtoclrbr 3295  fconst5 3962  fconstfv 3963  isomin 4013  isofrlem 4015  onfununi 4209  oecl 4308  oawordri 4320  omwordri 4339  odi 4346  unen 4575  mapenlem2 4637  pssnn 4681  brdom6disj 4951  cardinfima 5041  indpi 5188  1idpr 5287  prlem934a 5291  xrlttr 5707  infm3 6222  infmsup 6236  supxrre 6251  uzind 6376  uzwo4OLD 6381  qbtwnre 6418  uzwo 6582  uzwoOLD 6583  fzen 6622  sqlecan 6838  bccl2 7174  infpnlem1 7718  ruclem13 7734  infxpidmlem8 7771  isnei 7928  metequiv 8091  metcnss 8109  metelcls 8176  iscms2lem4 8203  bcthlem16 8225  bcthlem20 8229  occllem6 9454  nmcopexlem6 10235  nmcfnexlem6 10264  cnlnssadj 10292  atexch 10590  mdsymlem5 10616  elghomlem2 10668  mapudiscn 11015  cmpmon 11270  iepiclem 11278  trer 11409  elicc3 11410  finsschain 11425  ordiso 11426  cnsubsp2 11484  cptclsscpt 11489  subtopmetlem 11505  reconnlem5 11511  neibastop3 11585  fbssint 11626  neifg 11644  filssufillem 11655  filufint 11659  ufilen 11664  fcluscnp 11730  filnetlem4 11766  filnet 11768  inficl 11849  cnss 11953  isismty 12004  ismtyhmeo 12007  ismtyres 12010

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 145  df-an 223

Copyright terms: Public domain