Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orbi2d | GIF version |
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
orbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
orbi2d | ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbid.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | biimpd 143 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | orim2d 778 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
4 | 1 | biimprd 157 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 4 | orim2d 778 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓))) |
6 | 3, 5 | impbid 128 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∨ wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1d 781 orbi12d 783 dn1dc 949 xorbi2d 1369 eueq2dc 2894 r19.44mv 3498 rexprg 3622 rextpg 3624 exmidsssn 4175 exmidsssnc 4176 swopolem 4277 sowlin 4292 elsucg 4376 elsuc2g 4377 ordsoexmid 4533 poleloe 4997 isosolem 5786 freceq2 6352 brdifun 6519 pitric 7253 elinp 7406 prloc 7423 ltexprlemloc 7539 suplocexprlemloc 7653 ltsosr 7696 aptisr 7711 suplocsrlemb 7738 axpre-ltwlin 7815 axpre-suploclemres 7833 axpre-suploc 7834 gt0add 8462 apreap 8476 apreim 8492 elznn0 9197 elznn 9198 peano2z 9218 zindd 9300 elfzp1 9997 fzm1 10025 fzosplitsni 10160 cjap 10834 dvdslelemd 11766 zeo5 11810 lcmval 11974 lcmneg 11985 lcmass 11996 isprm6 12058 dedekindeulemloc 13144 dedekindeulemeu 13147 suplociccreex 13149 dedekindicclemloc 13153 dedekindicclemeu 13156 bj-charfunr 13533 bj-nn0sucALT 13701 |
Copyright terms: Public domain | W3C validator |