![]() |
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 502. (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 502 | . 2 ⊢ (𝜓 → (𝜒 → 𝜑)) |
3 | 2 | com12 32 | 1 ⊢ (𝜒 → (𝜓 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 398 |
This theorem is referenced by: xpidtr 6080 elovmporab 7603 elovmporab1w 7604 elovmporab1 7605 inficl 9369 cfslb2n 10212 repswcshw 14709 cshw1 14719 bezoutlem1 16428 bezoutlem3 16430 modprmn0modprm0 16687 insubm 18637 cnprest 22663 haust1 22726 lly1stc 22870 3cyclfrgrrn1 29278 dfon2lem9 34429 phpreu 36112 poimirlem26 36154 sb5ALT 42899 onfrALTlem2 42920 onfrALTlem2VD 43263 sb5ALTVD 43287 funcoressn 45366 ndmaovdistr 45529 2elfz3nn0 45638 |
Copyright terms: Public domain | W3C validator |