Theorem orim2i 540

Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)

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 22	. 2 |- ( ch -> ch )
2		orim1i.1	. 2 |- ( ph -> ps )
3	1, 2	orim12i 538	1 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 383

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

This theorem depends on definitions:  df-bi 197  df-or 385

This theorem is referenced by:  orbi2i  541  pm1.5  544  pm2.3  596  r19.44v  3094  elpwunsn  4224  elsuci  5791  ordnbtwnOLD  5817  infxpenlem  8836  fin1a2lem12  9233  fin1a2  9237  entri3  9381  zindd  11478  elfzr  12581  hashnn0pnf  13130  limccnp  23655  tgldimor  25397  ex-natded5.7-2  27269  chirredi  29253  meran1  32410  dissym1  32420  ordtoplem  32434  ordcmp  32446  poimirlem31  33440