| 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 1819 | . 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓) |
| 3 | 2 | albii 1819 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 |
| This theorem is referenced by: 3albii 1821 sbcom2 2173 2sb6rf 2478 mo4f 2567 2mo2 2647 2mos 2649 2mosOLD 2650 r3al 3197 ralcom 3289 ralcomf 3302 sbccomlem 3869 nfnid 5375 ssrel3 5796 raliunxp 5850 cnvsym 6132 cnvsymOLD 6133 cnvsymOLDOLD 6134 intasym 6135 intirr 6138 codir 6140 qfto 6141 dfpo2 6316 dffun4 6577 fun11 6640 fununi 6641 mpo2eqb 7565 frpoins3xpg 8165 xpord3inddlem 8179 aceq0 10158 zfac 10500 zfcndac 10659 addsrmo 11113 mulsrmo 11114 cotr2g 15015 isirred2 20421 isdomn3 20715 bnj580 34927 bnj978 34963 axacprim 35707 dfso2 35755 dfon2lem8 35791 dffun10 35915 wl-sbcom2d 37562 mpobi123f 38169 r2alan 38250 inxpss 38312 inxpss3 38315 cnvref5 38352 trcoss2 38485 dfantisymrel5 38763 antisymrelres 38764 dford4 43041 undmrnresiss 43617 cnvssco 43619 pm14.12 44440 ichn 47443 dfich2 47445 ichcom 47446 ichbi12i 47447 |
| Copyright terms: Public domain | W3C validator |