![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orcomd | GIF version |
Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.) |
Ref | Expression |
---|---|
orcomd.1 | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Ref | Expression |
---|---|
orcomd | ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcomd.1 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | |
2 | orcom 688 | . 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓)) | |
3 | 1, 2 | sylib 121 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 670 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: olcd 694 stabtestimpdc 868 pm5.54dc 871 swopo 4166 sotritrieq 4185 reg3exmidlemwe 4431 acexmidlemcase 5701 2oconcl 6266 nntri3or 6319 nntri2 6320 nntri1 6322 nnsseleq 6327 diffisn 6716 djulclb 6855 exmidomniim 6925 exmidomni 6926 addnqprlemfu 7269 mulnqprlemfu 7285 addcanprlemu 7324 cauappcvgprlemladdru 7365 apreap 8215 mulap0r 8243 mul0eqap 8292 nnm1nn0 8870 elnn0z 8919 zleloe 8953 nneoor 9005 nneo 9006 zeo2 9009 uzm1 9206 nn01to3 9259 uzsplit 9713 fzospliti 9794 fzouzsplit 9797 qavgle 9877 xrmaxiflemlub 10856 fz1f1o 10983 ef0lem 11164 zeo3 11360 bezoutlemmain 11479 unennn 11702 exmidunben 11731 nninfalllem1 12787 nninfall 12788 nninfsellemqall 12795 exmidsbthrlem 12801 sbthomlem 12804 trilpolemeq1 12817 |
Copyright terms: Public domain | W3C validator |