Theorem orim2i 766

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 764	1 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  767  pm1.5  770  pm2.3  780  ordi  821  dcn  847  pm2.25dc  898  dcand  938  axi12  1560  dveeq2or  1862  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  sbal1yz  2052  dvelimor  2069  exmodc  2128  r19.44av  2690  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  elsuci  4494  acexmidlemcase  6002  undifdcss  7096  updjudhf  7257  ctssdccl  7289  zindd  9576  fiubm  11063  lswex  11136  fsumsplitsn  11936  fprodcllem  12132  fprodsplitsn  12159  gsumwsubmcl  13544  gsumwmhm  13546  subctctexmid  16425