![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > albid | Structured version Visualization version GIF version |
Description: Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
albid.1 | ⊢ Ⅎ𝑥𝜑 |
albid.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
albid | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albid.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nf5ri 2183 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | albidh 1861 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 |
This theorem is referenced by: nfbidf 2212 dral1vOLD 2361 dral2 2431 dral1 2432 sb4b 2468 sbal1 2521 sbal2 2522 ralbidaOLD 3258 raleqf 3336 intab 4982 fin23lem32 10369 axrepndlem1 10617 axrepndlem2 10618 axrepnd 10619 axunnd 10621 axpowndlem2 10623 axpowndlem4 10625 axregndlem2 10628 axinfndlem1 10630 axinfnd 10631 axacndlem4 10635 axacndlem5 10636 axacnd 10637 iota5f 35449 exrecfnlem 36989 wl-equsald 37137 wl-equsaldv 37138 wl-sbnf1 37153 wl-2sb6d 37156 wl-sbalnae 37160 wl-mo2df 37168 wl-eudf 37170 wl-ax11-lem6 37188 wl-ax11-lem8 37190 ax12eq 38543 ax12el 38544 ax12v2-o 38551 unielss 42788 |
Copyright terms: Public domain | W3C validator |