Theorem orim2i 756

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

Syntax hints:   -> wi 4   \/ wo 703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi2i  757  pm1.5  760  pm2.3  770  ordi  811  dcn  837  pm2.25dc  888  dcan  928  axi12  1507  dveeq2or  1809  equs5or  1823  sb4or  1826  sb4bor  1828  nfsb2or  1830  sbequilem  1831  sbequi  1832  sbal1yz  1994  dvelimor  2011  exmodc  2069  r19.44av  2629  exmidundif  4192  exmidundifim  4193  elsuci  4388  acexmidlemcase  5848  undifdcss  6900  updjudhf  7056  ctssdccl  7088  zindd  9330  fiubm  10763  fsumsplitsn  11373  fprodcllem  11569  fprodsplitsn  11596  exmid1stab  14033  subctctexmid  14034