Theorem r19.26 3099

Description: Restricted quantifier version of 19.26 1877. (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 483	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 516	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 470	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3078	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 407	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 210	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3054

This theorem is referenced by:  r19.26-3  3100  ralbiim  3101  2ralbiim  3118  r19.26-2  3124  r19.27v  3168  r19.28v  3170  reu8  3674  ssrab  4002  r19.28z  4430  r19.27z  4438  ralnralall  4441  2reu4lem  4451  2ralunsn  4826  iuneq2  4941  disjxun  5070  triin  5196  asymref2  6067  cnvpo  6238  dfpo2  6247  fncnv  6558  fnres  6612  mptfnf  6620  fnopabg  6622  mpteqb  6955  eqfnfv3  6973  fvn0ssdmfun  7015  caoftrn  7661  poseq  8098  wfr3g  8259  iiner  8726  ixpeq2  8849  ixpin  8861  ixpfi2  9250  wemaplem2  9452  frr3g  9671  dfac5  10042  kmlem6  10069  eltsk2g  10665  intgru  10728  axgroth6  10742  fsequb  13928  rexanuz  15299  rexanre  15300  cau3lem  15308  rlimcn3  15543  o1of2  15566  o1rlimmul  15572  climbdd  15625  sqrt2irr  16207  gcdcllem1  16459  pc11  16842  prmreclem2  16879  catpropd  17666  issubc3  17807  fucinv  17934  ispos2  18272  issubg3  19111  issubg4  19112  pmtrdifwrdel2  19452  ringsrg  20269  iunocv  21656  cply1mul  22282  scmatf1  22514  cpmatsubgpmat  22703  tgval2  22939  1stcelcls  23444  ptclsg  23598  ptcnplem  23604  fbun  23823  txflf  23989  ucncn  24267  prdsmet  24353  metequiv  24492  metequiv2  24493  ncvsi  25136  iscau4  25264  cmetcaulem  25273  evthicc2  25445  ismbfcn  25614  mbfi1flimlem  25707  rolle  25975  itgsubst  26034  plydivex  26281  ulmcaulem  26377  ulmcau  26378  ulmbdd  26381  ulmcn  26382  mumullem2  27161  2sqlem6  27404  oldfib  28387  tgcgr4  28617  axpasch  29028  axeuclid  29050  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  vtxd0nedgb  29575  fusgrregdegfi  29656  rusgr1vtxlem  29674  uspgr2wlkeq  29732  wlkdlem4  29770  lfgriswlk  29773  frgrreg  30482  frgrregord013  30483  friendshipgt3  30486  ocsh  31372  spanuni  31633  riesz4i  32152  leopadd  32221  leoptri  32225  leoptr  32226  inpr0  32620  disjunsn  32683  voliune  34413  volfiniune  34414  eulerpartlemr  34558  eulerpartlemn  34565  nummin  35274  fmlasucdisj  35627  wzel  36050  neibastop1  36587  numiunnum  36698  phpreu  37971  ptrecube  37987  poimirlem23  38010  poimirlem27  38014  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  itg2addnc  38041  inixp  38095  rngoueqz  38307  intidl  38396  pclclN  40383  tendoeq2  41266  deg1gprod  42625  mzpincl  43183  lerabdioph  43250  ltrabdioph  43253  nerabdioph  43254  dvdsrabdioph  43255  dford3lem1  43471  gneispace  44578  ssrabf  45561  r19.28zf  45606  climxrre  46193  stoweidlem7  46450  stoweidlem54  46497  dirkercncflem3  46548  ply1mulgsumlem1  48877  ldepsnlinclem1  48996  ldepsnlinclem2  48997  iinxp  49321  nelsubc2  49559