![]() |
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 1895 | . 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓) |
3 | 2 | albii 1895 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∀wal 1629 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: sbcom2 2593 2sb6rf 2600 mo4f 2665 2mo2 2699 2mos 2701 r3al 3089 ralcomf 3244 nfnid 5025 raliunxp 5400 cnvsym 5651 intasym 5652 intirr 5655 codir 5657 qfto 5658 dffun4 6043 fun11 6103 fununi 6104 mpt22eqb 6916 aceq0 9141 zfac 9484 zfcndac 9643 addsrmo 10096 mulsrmo 10097 cotr2g 13925 isirred2 18909 rmo4fOLD 29675 bnj580 31321 bnj978 31357 axacprim 31922 dfso2 31982 dfpo2 31983 dfon2lem8 32031 dffun10 32358 wl-sbcom2d 33678 mpt2bi123f 34303 3albii 34356 ssrel3 34410 inxpss 34425 inxpss3 34427 trcoss2 34576 dford4 38122 isdomn3 38308 undmrnresiss 38436 cnvssco 38438 ntrneikb 38918 ntrneixb 38919 pm14.12 39148 |
Copyright terms: Public domain | W3C validator |