Theorem orc 707

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
orc	|- ( ph -> ( ph \/ ps ) )

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( ( ph \/ ps ) -> ( ph \/ ps ) )
2		jaob 705	. . 3 |- ( ( ( ph \/ ps ) -> ( ph \/ ps ) ) <-> ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) ) )
3	1, 2	mpbi 144	. 2 |- ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) )
4	3	simpli 110	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.67-2  708  pm1.4  722  orci  726  orcd  728  orcs  730  pm2.45  733  biorfi  741  pm1.5  760  pm2.4  773  pm4.44  774  pm4.78i  777  pm4.45  779  pm3.48  780  pm2.76  803  orabs  809  ordi  811  andi  813  pm4.72  822  biort  824  dcim  836  pm2.54dc  886  pm2.85dc  900  dcor  930  pm5.71dc  956  dedlema  964  3mix1  1161  xoranor  1372  19.33  1477  hbor  1539  nford  1560  19.30dc  1620  19.43  1621  19.32r  1673  moor  2090  r19.32r  2616  ssun1  3290  undif3ss  3388  reuun1  3409  prmg  3704  opthpr  3759  exmidn0m  4187  issod  4304  elelsuc  4394  ordtri2or2exmidlem  4510  regexmidlem1  4517  nndceq  6478  nndcel  6479  swoord1  6542  swoord2  6543  exmidontri2or  7220  addlocprlem  7497  msqge0  8535  mulge0  8538  ltleap  8551  nn1m1nn  8896  elnnz  9222  zletric  9256  zlelttric  9257  zmulcl  9265  zdceq  9287  zdcle  9288  zdclt  9289  ltpnf  9737  xrlttri3  9754  xrpnfdc  9799  xrmnfdc  9800  fzdcel  9996  qletric  10200  qlelttric  10201  qdceq  10203  qsqeqor  10586  hashfiv01gt1  10716  isum  11348  iprodap  11543  iprodap0  11545  nn0o1gt2  11864  prm23lt5  12217  bj-trdc  13787  bj-nn0suc0  13985  triap  14061  tridceq  14088