Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orbi2d | Structured version Visualization version GIF version |
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
bid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
orbi2d | ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | imbi2d 329 | . 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒))) |
3 | df-or 384 | . 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓)) | |
4 | df-or 384 | . 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 302 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-or 384 |
This theorem is referenced by: orbi1d 735 orbi12d 742 eueq2 3347 sbc2or 3411 r19.44zv 4021 rexprg 4182 rextpg 4184 swopolem 4968 poleloe 5446 elsucg 5709 elsuc2g 5710 brdifun 7658 brwdom 8355 isfin1a 8997 elgch 9323 suplem2pr 9754 axlttri 9988 mulcan1g 10559 elznn0 11269 elznn 11270 zindd 11354 rpneg 11739 dfle2 11856 fzm1 12289 fzosplitsni 12444 hashv01gt1 12995 zeo5 14918 bitsf1 15006 lcmval 15143 lcmneg 15154 lcmass 15165 isprm6 15264 infpn2 15455 irredmul 18532 domneq0 19118 znfld 19728 quotval 23851 plydivlem4 23855 plydivex 23856 aalioulem2 23892 aalioulem5 23895 aalioulem6 23896 aaliou 23897 aaliou2 23899 aaliou2b 23900 isinag 25529 axcontlem7 25650 hashecclwwlkn1 26361 eliccioo 28970 tlt2 28995 sibfof 29729 ballotlemfc0 29881 ballotlemfcc 29882 seglelin 31393 lineunray 31424 topdifinfeq 32374 mblfinlem2 32617 pridl 33006 maxidlval 33008 ispridlc 33039 pridlc 33040 dmnnzd 33044 lcfl7N 35808 aomclem8 36649 orbi1r 37737 iccpartgtl 39964 iccpartleu 39966 hashecclwwlksn1 41261 lindslinindsimp2lem5 42045 lindslinindsimp2 42046 |
Copyright terms: Public domain | W3C validator |