| 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 2195 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
| 3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 4 | 2, 3 | albidh 1866 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfbidf 2224 dral1vOLD 2373 dral2 2443 dral1 2444 sb4b 2480 sbal1 2533 sbal2 2534 ralbidaOLD 3271 raleqf 3353 intab 4978 fin23lem32 10384 axrepndlem1 10632 axrepndlem2 10633 axrepnd 10634 axunnd 10636 axpowndlem2 10638 axpowndlem4 10640 axregndlem2 10643 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 iota5f 35724 exrecfnlem 37380 wl-equsald 37540 wl-equsaldv 37541 wl-sbnf1 37556 wl-2sb6d 37559 wl-sbalnae 37563 wl-mo2df 37571 wl-eudf 37573 wl-ax11-lem6 37591 wl-ax11-lem8 37593 ax12eq 38942 ax12el 38943 ax12v2-o 38950 unielss 43230 |
| Copyright terms: Public domain | W3C validator |