Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2albii | GIF version |
Description: Inference adding 2 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 1446 | . 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓) |
3 | 2 | albii 1446 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∀wal 1329 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mor 2041 mo4f 2059 moanim 2073 2eu4 2092 ralcomf 2592 raliunxp 4680 cnvsym 4922 intasym 4923 intirr 4925 codir 4927 qfto 4928 dffun4 5134 dffun4f 5139 funcnveq 5186 fun11 5190 fununi 5191 mpo2eqb 5880 addnq0mo 7255 mulnq0mo 7256 addsrmo 7551 mulsrmo 7552 |
Copyright terms: Public domain | W3C validator |