Theorem orim2i 365

Description: Introduce disjunct to both sides of an implication.

Hypothesis

Ref	Expression
orim1i.1	|- (ph -> ps)

Assertion

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

Proof of Theorem orim2i

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (ch -> ch)
2		orim1i.1	. 2 |- (ph -> ps)
3	1, 2	orim12i 363	1 |- ((ch \/ ph) -> (ch \/ ps))

Syntax hints:   -> wi 3   \/ wo 239

This theorem is referenced by:  pm2.3 366  ordi 656  ordiOLD 657  r19.44av 2240  elsuci 3731  trsuc2 3754  ordnbtwn 3761  elpwunsn 3856  entri3 5992  zindd 7427  gxsuc 9395  irredi 11966  trsuc2OLD 13793  meran1 14235  dissym1 14245  nopsthph 14320  filcon 15580

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 164  df-or 241  df-an 242

Copyright terms: Public domain