Theorem r19.26-2 3136

Description: Restricted quantifier version of 19.26-2 1869. Version of r19.26 3109 with two quantifiers. (Contributed by NM, 10-Aug-2004.)

Assertion

Ref	Expression
r19.26-2	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))

Proof of Theorem r19.26-2

Step	Hyp	Ref	Expression
1		r19.26 3109	. . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓))
2	1	ralbii 3091	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓))
3		r19.26 3109	. 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
4	2, 3	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3060

This theorem is referenced by:  fununi  6643  tz7.48lem  8480  isffth2  17970  ispos2  18373  issgrpv  18747  issgrpn0  18748  isnsg2  19187  efgred  19781  isrnghm  20458  dfrhm2  20491  df2idl2rng  21284  cpmatacl  22738  cpmatmcllem  22740  caucfil  25331  aalioulem6  26394  ajmoi  30887  adjmo  31861  prmidl2  33449  iccllysconn  35235  dfso3  35700  fvineqsnf1  37393  ispridl2  38025  ishlat2  39335  fiinfi  43563  ntrk1k3eqk13  44040