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 699 | . . 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 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.67-2 702 pm1.4 716 orci 720 orcd 722 orcs 724 pm2.45 727 biorfi 735 pm1.5 754 pm2.4 767 pm4.44 768 pm4.78i 771 pm4.45 773 pm3.48 774 pm2.76 797 orabs 803 ordi 805 andi 807 pm4.72 812 biort 814 dcim 826 pm2.54dc 876 pm2.85dc 890 dcor 919 pm5.71dc 945 dedlema 953 3mix1 1150 xoranor 1355 19.33 1460 hbor 1525 nford 1546 19.30dc 1606 19.43 1607 19.32r 1658 moor 2068 r19.32r 2576 ssun1 3234 undif3ss 3332 reuun1 3353 prmg 3639 opthpr 3694 exmidn0m 4119 issod 4236 elelsuc 4326 ordtri2or2exmidlem 4436 regexmidlem1 4443 nndceq 6388 nndcel 6389 swoord1 6451 swoord2 6452 addlocprlem 7336 msqge0 8371 mulge0 8374 ltleap 8387 nn1m1nn 8731 elnnz 9057 zletric 9091 zlelttric 9092 zmulcl 9100 zdceq 9119 zdcle 9120 zdclt 9121 ltpnf 9560 xrlttri3 9576 xrpnfdc 9618 xrmnfdc 9619 fzdcel 9813 qletric 10014 qlelttric 10015 qdceq 10017 hashfiv01gt1 10521 isum 11147 nn0o1gt2 11591 bj-trdc 12948 bj-nn0suc0 13137 triap 13213 |
Copyright terms: Public domain | W3C validator |