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 1737 | . 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓) |
3 | 2 | albii 1737 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: sbcom2 2433 2sb6rf 2440 mo4f 2504 2mo2 2538 2mos 2540 r3al 2924 ralcomf 3077 nfnid 4823 raliunxp 5183 cnvsym 5429 intasym 5430 intirr 5433 codir 5435 qfto 5436 dffun4 5816 fun11 5877 fununi 5878 mpt22eqb 6667 aceq0 8824 zfac 9165 zfcndac 9320 addsrmo 9773 mulsrmo 9774 cotr2g 13563 isirred2 18524 2spotdisj 26588 rmo4fOLD 28720 bnj580 30237 bnj978 30273 axacprim 30838 dfso2 30897 dfpo2 30898 dfon2lem8 30939 dffun10 31191 wl-sbcom2d 32523 mpt2bi123f 33141 dford4 36614 isdomn3 36801 undmrnresiss 36929 cnvssco 36931 ntrneikb 37412 ntrneixb 37413 pm14.12 37644 |
Copyright terms: Public domain | W3C validator |