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 705 | . . 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 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 |
Copyright terms: Public domain | W3C validator |