![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simplbi2com | Structured version Visualization version GIF version |
Description: A deduction eliminating a conjunct, similar to simplbi2 499. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.) |
Ref | Expression |
---|---|
simplbi2com.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
simplbi2com | ⊢ (𝜒 → (𝜓 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbi2com.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | simplbi2 499 | . 2 ⊢ (𝜓 → (𝜒 → 𝜑)) |
3 | 2 | com12 32 | 1 ⊢ (𝜒 → (𝜓 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: xpidtr 6129 elovmporab 7667 elovmporab1w 7668 elovmporab1 7669 inficl 9450 cfslb2n 10293 repswcshw 14798 cshw1 14808 bezoutlem1 16518 bezoutlem3 16520 modprmn0modprm0 16779 insubm 18778 cnprest 23237 haust1 23300 lly1stc 23444 3cyclfrgrrn1 30167 dfon2lem9 35518 phpreu 37208 poimirlem26 37250 sb5ALT 44106 onfrALTlem2 44127 onfrALTlem2VD 44470 sb5ALTVD 44494 funcoressn 46562 ndmaovdistr 46725 2elfz3nn0 46834 |
Copyright terms: Public domain | W3C validator |