Theorem r19.26 3111

Description: Restricted quantifier version of 19.26 1870. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

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

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		simpl 482	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 511	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 469	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3085	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 406	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

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

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  df-an 396  df-ral 3062

This theorem is referenced by:  r19.26-3  3112  ralbiim  3113  2ralbiim  3132  r19.26-2  3138  r19.27v  3188  r19.28v  3190  reu8  3739  ssrab  4073  r19.28z  4498  r19.27z  4505  ralf0  4514  ralnralall  4515  2reu4lem  4522  2ralunsn  4895  iuneq2  5011  disjxun  5141  triin  5276  asymref2  6137  cnvpo  6307  dfpo2  6316  fncnv  6639  fnres  6695  mptfnf  6703  fnopabg  6705  mpteqb  7035  eqfnfv3  7053  fvn0ssdmfun  7094  caoftrn  7738  poseq  8183  wfr3g  8347  iiner  8829  ixpeq2  8951  ixpin  8963  ixpfi2  9390  wemaplem2  9587  frr3g  9796  dfac5  10169  kmlem6  10196  eltsk2g  10791  intgru  10854  axgroth6  10868  fsequb  14016  rexanuz  15384  rexanre  15385  cau3lem  15393  rlimcn3  15626  o1of2  15649  o1rlimmul  15655  climbdd  15708  sqrt2irr  16285  gcdcllem1  16536  pc11  16918  prmreclem2  16955  catpropd  17752  issubc3  17894  fucinv  18021  ispos2  18361  issubg3  19162  issubg4  19163  pmtrdifwrdel2  19504  ringsrg  20294  iunocv  21699  cply1mul  22300  scmatf1  22537  cpmatsubgpmat  22726  tgval2  22963  1stcelcls  23469  ptclsg  23623  ptcnplem  23629  fbun  23848  txflf  24014  ucncn  24294  prdsmet  24380  metequiv  24522  metequiv2  24523  ncvsi  25185  iscau4  25313  cmetcaulem  25322  evthicc2  25495  ismbfcn  25664  mbfi1flimlem  25757  rolle  26028  itgsubst  26090  plydivex  26339  ulmcaulem  26437  ulmcau  26438  ulmbdd  26441  ulmcn  26442  mumullem2  27223  2sqlem6  27467  tgcgr4  28539  axpasch  28956  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  vtxd0nedgb  29506  fusgrregdegfi  29587  rusgr1vtxlem  29605  uspgr2wlkeq  29664  wlkdlem4  29703  lfgriswlk  29706  frgrreg  30413  frgrregord013  30414  friendshipgt3  30417  ocsh  31302  spanuni  31563  riesz4i  32082  leopadd  32151  leoptri  32155  leoptr  32156  inpr0  32550  disjunsn  32607  voliune  34230  volfiniune  34231  eulerpartlemr  34376  eulerpartlemn  34383  nummin  35105  fmlasucdisj  35404  wzel  35825  neibastop1  36360  numiunnum  36471  phpreu  37611  ptrecube  37627  poimirlem23  37650  poimirlem27  37654  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnc  37681  inixp  37735  rngoueqz  37947  intidl  38036  pclclN  39893  tendoeq2  40776  deg1gprod  42141  mzpincl  42745  lerabdioph  42816  ltrabdioph  42819  nerabdioph  42820  dvdsrabdioph  42821  dford3lem1  43038  gneispace  44147  ssrabf  45119  r19.28zf  45164  climxrre  45765  stoweidlem7  46022  stoweidlem54  46069  dirkercncflem3  46120  ply1mulgsumlem1  48303  ldepsnlinclem1  48422  ldepsnlinclem2  48423