Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprbda | Structured version Visualization version GIF version |
Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
Ref | Expression |
---|---|
pm3.26bda.1 | ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) |
Ref | Expression |
---|---|
simprbda | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.26bda.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | |
2 | 1 | biimpa 477 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃)) |
3 | 2 | simpld 495 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 |
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 397 |
This theorem is referenced by: elrabiOLD 3620 oteqex 5415 fsnex 7164 fisupg 9071 fiinfg 9267 cantnff 9441 fseqenlem2 9790 fpwwe2lem10 10405 fpwwe2lem11 10406 fpwwe2 10408 rlimsqzlem 15369 ramub1lem2 16737 mriss 17353 invfun 17485 pltle 18060 subgslw 19230 frgpnabllem2 19484 cyggeninv 19492 ablfaclem3 19699 lmodfopnelem1 20168 pjff 20928 pjf2 20930 pjfo 20931 pjcss 20932 psrbagfOLD 21131 mplind 21287 mhpmpl 21343 fvmptnn04ifc 22010 chfacfisf 22012 chfacfisfcpmat 22013 tg1 22123 cldss 22189 cnf2 22409 cncnp 22440 lly1stc 22656 refbas 22670 qtoptop2 22859 qtoprest 22877 elfm3 23110 flfelbas 23154 cnextf 23226 restutopopn 23399 cfilufbas 23450 fmucnd 23453 blgt0 23561 xblss2ps 23563 xblss2 23564 tngngp 23827 cfilfil 24440 iscau2 24450 caufpm 24455 cmetcaulem 24461 dvcnp2 25093 dvfsumrlim 25204 dvfsumrlim2 25205 fta1g 25341 dvdsflsumcom 26346 fsumvma 26370 vmadivsumb 26640 dchrisumlema 26645 dchrvmasumlem1 26652 dchrvmasum2lem 26653 dchrvmasumiflem1 26658 selbergb 26706 selberg2b 26709 pntibndlem3 26749 pntlem3 26766 motgrp 26913 oppnid 27116 sspnv 29097 lnof 29126 bloln 29155 dfmgc2 31283 fldexttr 31742 reff 31798 signsply0 32539 cvmliftmolem1 33252 cvmlift2lem9a 33274 mbfresfi 35832 itg2gt0cn 35841 ismtyres 35975 ghomf 36057 rngoisohom 36147 pridlidl 36202 pridlnr 36203 maxidlidl 36208 lflf 37084 lkrcl 37113 cvrlt 37291 cvrle 37299 atbase 37310 llnbase 37530 lplnbase 37555 lvolbase 37599 psubssat 37775 lhpbase 38019 laut1o 38106 ldillaut 38132 ltrnldil 38143 diadmclN 39058 pell1234qrre 40681 lnmlsslnm 40913 cvgdvgrat 41938 stoweidlem34 43582 mpbiran3d 46153 |
Copyright terms: Public domain | W3C validator |