| 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 340 | . 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒))) |
| 3 | df-or 849 | . 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓)) | |
| 4 | df-or 849 | . 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 848 |
| 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 207 df-or 849 |
| This theorem is referenced by: orbi1d 917 orbi12d 919 eueq2 3716 sbc2or 3797 r19.44zv 4504 elunsn 4683 rexprgf 4695 rextpg 4699 swopolem 5602 poleloe 6151 elsucg 6452 elsuc2g 6453 xpord2indlem 8172 brdifun 8775 brwdom 9607 isfin1a 10332 elgch 10662 suplem2pr 11093 axlttri 11332 mulcan1g 11916 elznn0 12628 elznn 12629 zindd 12719 rpneg 13067 dfle2 13189 fzm1 13647 fzosplitsni 13817 hashv01gt1 14384 zeo5 16393 bitsf1 16483 lcmval 16629 lcmneg 16640 lcmass 16651 isprm6 16751 infpn2 16951 irredmul 20429 lringuplu 20544 domneq0 20708 znfld 21579 quotval 26334 plydivlem4 26338 plydivex 26339 aalioulem2 26375 aalioulem5 26378 aalioulem6 26379 aaliou 26380 aaliou2 26382 aaliou2b 26383 elzs2 28385 elznns 28388 isinag 28846 axcontlem7 28985 hashecclwwlkn1 30096 eliccioo 32913 tlt2 32959 prmidl 33468 mxidlval 33489 rprmdvds 33547 sibfof 34342 ballotlemfc0 34495 ballotlemfcc 34496 satfvsucsuc 35370 satf0op 35382 fmlafvel 35390 isfmlasuc 35393 satfv1fvfmla1 35428 seglelin 36117 lineunray 36148 topdifinfeq 37351 wl-ifp4impr 37468 mblfinlem2 37665 pridl 38044 maxidlval 38046 ispridlc 38077 pridlc 38078 dmnnzd 38082 lcfl7N 41503 aomclem8 43073 fzuntgd 43471 orbi1r 44530 iccpartgtl 47413 iccpartleu 47415 clnbupgrel 47821 dfsclnbgr6 47844 lindslinindsimp2lem5 48379 lindslinindsimp2 48380 rrx2pnedifcoorneorr 48638 |
| Copyright terms: Public domain | W3C validator |