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 342 | . 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒))) |
3 | df-or 842 | . 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓)) | |
4 | df-or 842 | . 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 315 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: orbi1d 910 orbi12d 912 eueq2 3698 sbc2or 3778 r19.44zv 4445 rexprgf 4623 rextpg 4627 swopolem 5476 poleloe 5984 elsucg 6251 elsuc2g 6252 brdifun 8307 brwdom 9019 isfin1a 9702 elgch 10032 suplem2pr 10463 axlttri 10700 mulcan1g 11281 elznn0 11984 elznn 11985 zindd 12071 rpneg 12409 dfle2 12528 fzm1 12975 fzosplitsni 13136 hashv01gt1 13693 zeo5 15693 bitsf1 15783 lcmval 15924 lcmneg 15935 lcmass 15946 isprm6 16046 infpn2 16237 irredmul 19388 domneq0 19998 znfld 20635 quotval 24808 plydivlem4 24812 plydivex 24813 aalioulem2 24849 aalioulem5 24852 aalioulem6 24853 aaliou 24854 aaliou2 24856 aaliou2b 24857 isinag 26551 axcontlem7 26683 hashecclwwlkn1 27783 elunsn 30200 eliccioo 30534 tlt2 30578 prmidl 30876 sibfof 31497 ballotlemfc0 31649 ballotlemfcc 31650 satfvsucsuc 32509 satf0op 32521 fmlafvel 32529 isfmlasuc 32532 satfv1fvfmla1 32567 seglelin 33474 lineunray 33505 topdifinfeq 34513 mblfinlem2 34811 pridl 35196 maxidlval 35198 ispridlc 35229 pridlc 35230 dmnnzd 35234 lcfl7N 38517 aomclem8 39539 orbi1r 40721 iccpartgtl 43463 iccpartleu 43465 lindslinindsimp2lem5 44445 lindslinindsimp2 44446 rrx2pnedifcoorneorr 44632 |
Copyright terms: Public domain | W3C validator |