![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > albidv | Structured version Visualization version GIF version |
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
albidv | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1988 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1942 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: 2albidv 2000 ax12wdemo 2161 eujust 2609 eujustALT 2610 euf 2615 mo2 2616 axext3 2742 axext3ALT 2743 bm1.1 2745 eqeq1dALT 2763 nfceqdf 2898 ralbidv2 3122 ralxpxfr2d 3466 alexeqg 3471 pm13.183 3484 eqeu 3518 mo2icl 3526 euind 3534 reuind 3552 cdeqal 3565 sbcal 3626 sbcabel 3658 csbiebg 3697 ssconb 3886 reldisj 4163 sbcssg 4229 elint 4633 axrep1 4924 axrep2 4925 axrep3 4926 axrep4 4927 zfrepclf 4929 axsep2 4934 zfauscl 4935 bm1.3ii 4936 eusv1 5009 euotd 5123 freq1 5236 frsn 5346 iota5 6032 sbcfung 6073 funimass4 6410 dffo3 6538 eufnfv 6655 dff13 6676 tfisi 7224 dfom2 7233 elom 7234 seqomlem2 7716 pssnn 8345 findcard 8366 findcard2 8367 findcard3 8370 fiint 8404 inf0 8693 axinf2 8712 tz9.1 8780 karden 8933 aceq0 9151 dfac5 9161 zfac 9494 brdom3 9562 axpowndlem3 9633 zfcndrep 9648 zfcndac 9653 elgch 9656 engch 9662 axgroth3 9865 axgroth4 9866 elnp 10021 elnpi 10022 infm3 11194 fz1sbc 12629 uzrdgfni 12971 trclfvcotr 13969 relexpindlem 14022 vdwmc2 15905 ramtlecl 15926 ramval 15934 ramub 15939 rami 15941 ramcl 15955 mreexexd 16530 mplsubglem 19656 mpllsslem 19657 istopg 20922 1stccn 21488 iskgen3 21574 fbfinnfr 21866 cnextfun 22089 metcld 23324 metcld2 23325 chlimi 28421 nmcexi 29215 disjrdx 29732 funcnvmpt 29798 mclsssvlem 31787 mclsval 31788 mclsind 31795 elintfv 31990 dfon2lem6 32019 dfon2lem7 32020 dfon2lem8 32021 dfon2 32023 sscoid 32347 trer 32637 bj-ssbjust 32946 bj-ssbequ 32957 bj-ssblem1 32958 bj-axext3 33097 bj-axrep1 33116 bj-axrep2 33117 bj-axrep3 33118 bj-axrep4 33119 bj-sbceqgALT 33219 bj-axsep2 33245 bj-nuliota 33343 wl-mo2t 33688 isass 33976 releccnveq 34364 ecin0 34458 inecmo 34461 alrmomodm 34465 extssr 34600 axc11n-16 34745 cdlemefrs29bpre0 36204 elmapintab 38422 cnvcnvintabd 38426 iunrelexpuztr 38531 ntrneiiso 38909 ntrneik2 38910 ntrneix2 38911 ntrneikb 38912 pm14.122b 39144 iotavalb 39151 trsbc 39270 sbcalgOLD 39272 sbcssOLD 39276 dffo3f 39881 fun2dmnopgexmpl 41829 setrecseq 42960 setrec1lem1 42962 setrec2fun 42967 setrec2lem2 42969 |
Copyright terms: Public domain | W3C validator |