Theorem orim2i 518

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

Hypothesis

Ref	Expression
orim1i.1

Assertion

Ref	Expression
orim2i

Proof of Theorem orim2i

Step	Hyp	Ref	Expression
1		id 22	. 2
2		orim1i.1	. 2
3	1, 2	orim12i 516	1

Syntax hints:  ->wi 4  \/wo 368

This theorem is referenced by:  orbi2i  519  pm1.5  522  pm2.3  572  r19.44v  3014  elpwunsn  4070  elsuci  4949  ordnbtwn  4973  infxpenlem  8412  fin1a2lem12  8812  fin1a2  8816  entri3  8955  zindd  10990  hashnn0pnf  12415  limccnp  22295  tgldimor  23893  ex-natded5.7-2  25133  gxsuc  25274  chirredi  27313  meran1  29876  dissym1  29886  ordtoplem  29900  ordcmp  29912

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 185  df-or 370