![]() |
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 496. (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 496 | . 2 ⊢ (𝜓 → (𝜒 → 𝜑)) |
3 | 2 | com12 32 | 1 ⊢ (𝜒 → (𝜓 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 387 |
This theorem is referenced by: elresOLD 5672 xpidtr 5760 elovmpt2rab 7140 elovmpt2rab1 7141 inficl 8600 cfslb2n 9405 repswcshw 13933 cshw1 13943 bezoutlem1 15629 bezoutlem3 15631 modprmn0modprm0 15883 cnprest 21464 haust1 21527 lly1stc 21670 3cyclfrgrrn1 27666 dfon2lem9 32234 phpreu 33936 poimirlem26 33979 sb5ALT 39569 onfrALTlem2 39590 onfrALTlem2VD 39943 sb5ALTVD 39967 funcoressn 41973 ndmaovdistr 42109 2elfz3nn0 42214 |
Copyright terms: Public domain | W3C validator |