Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orc | GIF version |
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
orc | ⊢ (𝜑 → (𝜑 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓)) | |
2 | jaob 700 | . . 3 ⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜓)) ↔ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓)))) | |
3 | 1, 2 | mpbi 144 | . 2 ⊢ ((𝜑 → (𝜑 ∨ 𝜓)) ∧ (𝜓 → (𝜑 ∨ 𝜓))) |
4 | 3 | simpli 110 | 1 ⊢ (𝜑 → (𝜑 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∨ wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.67-2 703 pm1.4 717 orci 721 orcd 723 orcs 725 pm2.45 728 biorfi 736 pm1.5 755 pm2.4 768 pm4.44 769 pm4.78i 772 pm4.45 774 pm3.48 775 pm2.76 798 orabs 804 ordi 806 andi 808 pm4.72 813 biort 815 dcim 827 pm2.54dc 877 pm2.85dc 891 dcor 920 pm5.71dc 946 dedlema 954 3mix1 1151 xoranor 1359 19.33 1464 hbor 1526 nford 1547 19.30dc 1607 19.43 1608 19.32r 1660 moor 2077 r19.32r 2603 ssun1 3270 undif3ss 3368 reuun1 3389 prmg 3680 opthpr 3735 exmidn0m 4162 issod 4279 elelsuc 4369 ordtri2or2exmidlem 4485 regexmidlem1 4492 nndceq 6446 nndcel 6447 swoord1 6509 swoord2 6510 exmidontri2or 7178 addlocprlem 7455 msqge0 8491 mulge0 8494 ltleap 8507 nn1m1nn 8851 elnnz 9177 zletric 9211 zlelttric 9212 zmulcl 9220 zdceq 9239 zdcle 9240 zdclt 9241 ltpnf 9687 xrlttri3 9704 xrpnfdc 9746 xrmnfdc 9747 fzdcel 9942 qletric 10143 qlelttric 10144 qdceq 10146 hashfiv01gt1 10656 isum 11282 iprodap 11477 iprodap0 11479 nn0o1gt2 11796 bj-trdc 13335 bj-nn0suc0 13536 triap 13611 tridceq 13638 |
Copyright terms: Public domain | W3C validator |