| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpbidi | Structured version Visualization version GIF version | ||
| Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.) |
| Ref | Expression |
|---|---|
| mpbidi.min | ⊢ (𝜃 → (𝜑 → 𝜓)) |
| mpbidi.maj | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| mpbidi | ⊢ (𝜃 → (𝜑 → 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpbidi.min | . 2 ⊢ (𝜃 → (𝜑 → 𝜓)) | |
| 2 | mpbidi.maj | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 3 | 2 | biimpd 229 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 4 | 1, 3 | sylcom 30 | 1 ⊢ (𝜃 → (𝜑 → 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 |
| This theorem is referenced by: ralxfr2d 5410 ovmpt4g 7580 ov3 7596 omeulem2 8621 domtriomlem 10482 nsmallnq 11017 bposlem1 27328 pntrsumbnd 27610 elntg2 29000 mptsnunlem 37339 poimirlem27 37654 refressn 38444 frege92 43968 nzss 44336 modelaxreplem1 44995 ormklocald 46889 setis 49217 |
| Copyright terms: Public domain | W3C validator |