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 480 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃)) |
3 | 2 | simpld 498 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: elrabiOLD 3580 oteqex 5354 fsnex 7044 fisupg 8833 fiinfg 9029 cantnff 9203 fseqenlem2 9518 fpwwe2lem10 10133 fpwwe2lem11 10134 fpwwe2 10136 rlimsqzlem 15091 ramub1lem2 16456 mriss 17002 invfun 17132 pltle 17680 subgslw 18852 frgpnabllem2 19106 cyggeninv 19114 ablfaclem3 19321 lmodfopnelem1 19782 pjff 20521 pjf2 20523 pjfo 20524 pjcss 20525 psrbagfOLD 20725 mplind 20875 mhpmpl 20931 fvmptnn04ifc 21596 chfacfisf 21598 chfacfisfcpmat 21599 tg1 21708 cldss 21773 cnf2 21993 cncnp 22024 lly1stc 22240 refbas 22254 qtoptop2 22443 qtoprest 22461 elfm3 22694 flfelbas 22738 cnextf 22810 restutopopn 22983 cfilufbas 23034 fmucnd 23037 blgt0 23145 xblss2ps 23147 xblss2 23148 tngngp 23400 cfilfil 24012 iscau2 24022 caufpm 24027 cmetcaulem 24033 dvcnp2 24664 dvfsumrlim 24775 dvfsumrlim2 24776 fta1g 24912 dvdsflsumcom 25917 fsumvma 25941 vmadivsumb 26211 dchrisumlema 26216 dchrvmasumlem1 26223 dchrvmasum2lem 26224 dchrvmasumiflem1 26229 selbergb 26277 selberg2b 26280 pntibndlem3 26320 pntlem3 26337 motgrp 26481 oppnid 26684 sspnv 28653 lnof 28682 bloln 28711 dfmgc2 30843 fldexttr 31297 reff 31353 signsply0 32092 cvmliftmolem1 32806 cvmlift2lem9a 32828 mbfresfi 35435 itg2gt0cn 35444 ismtyres 35578 ghomf 35660 rngoisohom 35750 pridlidl 35805 pridlnr 35806 maxidlidl 35811 lflf 36689 lkrcl 36718 cvrlt 36896 cvrle 36904 atbase 36915 llnbase 37135 lplnbase 37160 lvolbase 37204 psubssat 37380 lhpbase 37624 laut1o 37711 ldillaut 37737 ltrnldil 37748 diadmclN 38663 pell1234qrre 40230 lnmlsslnm 40462 cvgdvgrat 41453 stoweidlem34 43101 monepilem 45660 |
Copyright terms: Public domain | W3C validator |