| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > biadanii | Structured version Visualization version GIF version | ||
| Description: Inference associated with biadani 820. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.) |
| Ref | Expression |
|---|---|
| biadani.1 | ⊢ (𝜑 → 𝜓) |
| biadanii.2 | ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| biadanii | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biadanii.2 | . 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) | |
| 2 | biadani.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 3 | 2 | biadani 820 | . 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))) |
| 4 | 1, 3 | mpbi 230 | 1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: elab4g 3683 elpwb 4608 ssdifsn 4788 brab2a 5779 elon2 6395 elovmpo 7678 eqop2 8057 iscard 10015 iscard2 10016 elnnnn0 12569 elfzo2 13702 bitsval 16461 1nprm 16716 funcpropd 17947 isfull 17957 isfth 17961 ismgmhm 18709 ismhm 18798 isghm 19233 isghmOLD 19234 ghmpropd 19274 isga 19309 oppgcntz 19383 gexdvdsi 19601 isrnghm 20441 isrhm 20478 issdrg 20789 abvpropd 20836 islmhm 21026 dfprm2 21484 prmirred 21485 elocv 21686 isobs 21740 iscn2 23246 iscnp2 23247 islocfin 23525 elflim2 23972 isfcls 24017 isnghm 24744 isnmhm 24767 0plef 25707 elply 26234 dchrelbas4 27287 brsslt 27830 nb3grpr 29399 ispligb 30496 isph 30841 abfmpunirn 32662 iscvm 35264 sscoid 35914 bj-pwvrelb 36899 bj-elsnb 37062 bj-ideqb 37160 bj-opelidb1ALT 37167 bj-elid5 37170 eldiophb 42768 eldioph3b 42776 eldioph4b 42822 bropabg 43336 brfvrcld2 43705 |
| Copyright terms: Public domain | W3C validator |