![]() |
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 3677 oteqex 5499 fsnex 7277 fisupg 9287 fiinfg 9490 cantnff 9665 fseqenlem2 10016 fpwwe2lem10 10631 fpwwe2lem11 10632 fpwwe2 10634 rlimsqzlem 15591 ramub1lem2 16956 mriss 17575 invfun 17707 pltle 18282 subgslw 19478 frgpnabllem2 19736 cyggeninv 19745 ablfaclem3 19951 lmodfopnelem1 20500 pjff 21258 pjf2 21260 pjfo 21261 pjcss 21262 psrbagfOLD 21463 mplind 21622 mhpmpl 21678 fvmptnn04ifc 22345 chfacfisf 22347 chfacfisfcpmat 22348 tg1 22458 cldss 22524 cnf2 22744 cncnp 22775 lly1stc 22991 refbas 23005 qtoptop2 23194 qtoprest 23212 elfm3 23445 flfelbas 23489 cnextf 23561 restutopopn 23734 cfilufbas 23785 fmucnd 23788 blgt0 23896 xblss2ps 23898 xblss2 23899 tngngp 24162 cfilfil 24775 iscau2 24785 caufpm 24790 cmetcaulem 24796 dvcnp2 25428 dvfsumrlim 25539 dvfsumrlim2 25540 fta1g 25676 dvdsflsumcom 26681 fsumvma 26705 vmadivsumb 26975 dchrisumlema 26980 dchrvmasumlem1 26987 dchrvmasum2lem 26988 dchrvmasumiflem1 26993 selbergb 27041 selberg2b 27044 pntibndlem3 27084 pntlem3 27101 motgrp 27783 oppnid 27986 sspnv 29966 lnof 29995 bloln 30024 dfmgc2 32153 fldexttr 32725 reff 32807 signsply0 33550 cvmliftmolem1 34260 cvmlift2lem9a 34282 gg-dvcnp2 35162 mbfresfi 36522 itg2gt0cn 36531 ismtyres 36664 ghomf 36746 rngoisohom 36836 pridlidl 36891 pridlnr 36892 maxidlidl 36897 lflf 37921 lkrcl 37950 cvrlt 38128 cvrle 38136 atbase 38147 llnbase 38368 lplnbase 38393 lvolbase 38437 psubssat 38613 lhpbase 38857 laut1o 38944 ldillaut 38970 ltrnldil 38981 diadmclN 39896 pell1234qrre 41575 lnmlsslnm 41808 cantnf2 42060 naddcnfid1 42102 cvgdvgrat 43057 stoweidlem34 44736 mpbiran3d 47435 |
Copyright terms: Public domain | W3C validator |