![]() |
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 495. (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 495 | . 2 ⊢ (𝜓 → (𝜒 → 𝜑)) |
3 | 2 | com12 32 | 1 ⊢ (𝜒 → (𝜓 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: elresOLD 5646 xpidtr 5736 elovmpt2rab 7114 elovmpt2rab1 7115 inficl 8573 cfslb2n 9378 repswcshw 13897 cshw1 13907 bezoutlem1 15591 bezoutlem3 15593 modprmn0modprm0 15845 cnprest 21422 haust1 21485 lly1stc 21628 3cyclfrgrrn1 27634 dfon2lem9 32208 phpreu 33882 poimirlem26 33924 sb5ALT 39511 onfrALTlem2 39532 onfrALTlem2VD 39885 sb5ALTVD 39909 funcoressn 41925 ndmaovdistr 42061 2elfz3nn0 42166 |
Copyright terms: Public domain | W3C validator |