![]() |
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 5416 ovmpt4g 7580 ov3 7596 omeulem2 8620 domtriomlem 10480 nsmallnq 11015 bposlem1 27343 pntrsumbnd 27625 elntg2 29015 mptsnunlem 37321 poimirlem27 37634 refressn 38425 frege92 43945 nzss 44313 modelaxreplem1 44943 setis 48929 |
Copyright terms: Public domain | W3C validator |