Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2albii | Structured version Visualization version GIF version |
Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
albii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2albii | ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | albii 1811 | . 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓) |
3 | 2 | albii 1811 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 |
This theorem is referenced by: sbcom2 2158 2sb6rf 2489 2sb6rfOLD 2490 mo4f 2644 2mo2 2725 2mos 2727 r3al 3199 ralcom 3351 ralcomf 3354 nfnid 5267 raliunxp 5703 cnvsym 5967 intasym 5968 intirr 5971 codir 5973 qfto 5974 dffun4 6360 fun11 6421 fununi 6422 mpo2eqb 7272 aceq0 9532 zfac 9870 zfcndac 10029 addsrmo 10483 mulsrmo 10484 cotr2g 14324 isirred2 19380 bnj580 32084 bnj978 32120 axacprim 32830 dfso2 32887 dfpo2 32888 dfon2lem8 32932 dffun10 33272 wl-sbcom2d 34678 mpobi123f 35321 3albii 35390 ssrel3 35437 inxpss 35450 inxpss3 35452 trcoss2 35604 dford4 39504 isdomn3 39682 undmrnresiss 39842 cnvssco 39844 pm14.12 40630 dfich2 43490 dfich2ai 43491 ichcom 43494 ichbi12i 43495 ichn 43503 |
Copyright terms: Public domain | W3C validator |