![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orbi12d | GIF version |
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
orbi12d.1 | ⊢ (φ → (ψ ↔ χ)) |
orbi12d.2 | ⊢ (φ → (θ ↔ τ)) |
Ref | Expression |
---|---|
orbi12d | ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ τ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi12d.1 | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
2 | 1 | orbi1d 704 | . 2 ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ θ))) |
3 | orbi12d.2 | . . 3 ⊢ (φ → (θ ↔ τ)) | |
4 | 3 | orbi2d 703 | . 2 ⊢ (φ → ((χ ∨ θ) ↔ (χ ∨ τ))) |
5 | 2, 4 | bitrd 177 | 1 ⊢ (φ → ((ψ ∨ θ) ↔ (χ ∨ τ))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∨ wo 628 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm4.39 734 dcbid 747 3orbi123d 1205 dfbi3dc 1285 eueq3dc 2709 sbcor 2801 sbcorg 2802 unjust 2915 elun 3078 ifbi 3342 elprg 3384 eltpg 3407 rabrsndc 3429 preq12bg 3535 swopolem 4033 soeq1 4043 sowlin 4048 ordtri2orexmid 4211 regexmidlemm 4217 regexmidlem1 4218 ordsoexmid 4240 nn0suc 4270 nndceq0 4282 0elnn 4283 soinxp 4353 fununi 4910 funcnvuni 4911 fun11iun 5090 unpreima 5235 isosolem 5406 xporderlem 5793 poxp 5794 frec0g 5922 frecsuclem3 5929 frecsuc 5930 indpi 6326 ltexprlemloc 6581 addextpr 6593 ltsosr 6692 aptisr 6705 mulextsr1lem 6706 mulextsr1 6707 axpre-ltwlin 6767 axpre-apti 6769 axpre-mulext 6772 axltwlin 6884 axapti 6887 reapval 7360 reapti 7363 reapmul1lem 7378 reapmul1 7379 reapadd1 7380 reapneg 7381 reapcotr 7382 remulext1 7383 apreim 7387 apsym 7390 apcotr 7391 apadd1 7392 addext 7394 apneg 7395 nn1m1nn 7713 nn1gt1 7728 elznn0 8036 elz2 8088 nn0n0n1ge2b 8096 nneoor 8116 uztric 8270 ltxr 8465 fzsplit2 8684 uzsplit 8724 fzospliti 8802 fzouzsplit 8805 bj-dcbi 9383 bj-nn0suc0 9410 bj-inf2vnlem2 9431 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |