Theorem orc 712

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 710	. . 3 |- ( ( ( ph \/ ps ) -> ( ph \/ ps ) ) <-> ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) ) )
3	1, 2	mpbi 145	. 2 |- ( ( ph -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ps ) ) )
4	3	simpli 111	1 |- ( ph -> ( ph \/ ps ) )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.67-2  713  pm1.4  727  orci  731  orcd  733  orcs  735  pm2.45  738  biorfi  746  pm1.5  765  pm2.4  778  pm4.44  779  pm4.78i  782  pm4.45  784  pm3.48  785  pm2.76  808  orabs  814  ordi  816  andi  818  pm4.72  827  biort  829  dcim  841  pm2.54dc  891  pm2.85dc  905  dcor  935  pm5.71dc  961  dedlema  969  3mix1  1166  xoranor  1377  19.33  1484  hbor  1546  nford  1567  19.30dc  1627  19.43  1628  19.32r  1680  moor  2097  r19.32r  2623  ssun1  3300  undif3ss  3398  reuun1  3419  prmg  3715  opthpr  3774  exmidn0m  4203  issod  4321  elelsuc  4411  ordtri2or2exmidlem  4527  regexmidlem1  4534  nndceq  6502  nndcel  6503  swoord1  6566  swoord2  6567  exmidontri2or  7244  addlocprlem  7536  msqge0  8575  mulge0  8578  ltleap  8591  nn1m1nn  8939  elnnz  9265  zletric  9299  zlelttric  9300  zmulcl  9308  zdceq  9330  zdcle  9331  zdclt  9332  ltpnf  9782  xrlttri3  9799  xrpnfdc  9844  xrmnfdc  9845  fzdcel  10042  qletric  10246  qlelttric  10247  qdceq  10249  qsqeqor  10633  hashfiv01gt1  10764  isum  11395  iprodap  11590  iprodap0  11592  nn0o1gt2  11912  prm23lt5  12265  bj-trdc  14589  bj-nn0suc0  14787  triap  14862  tridceq  14889