Theorem r19.26 3127

Description: Restricted quantifier version of 19.26 1903. (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 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3104	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3104	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 521	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 475	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3106	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 412	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3082

This theorem is used by:  r19.26-3  3128  ralbiim  3129  2ralbiim  3146  r19.26-2  3152  r19.27v  3196  r19.28v  3198  reu8  3698  ssrab  4026  r19.28z  4465  r19.27z  4473  ralnralall  4476  2reu4lem  4486  2ralunsn  4862  iuneq2  4978  disjxun  5109  triin  5237  asymref2  6119  cnvpo  6292  dfpo2  6301  fncnv  6613  fnres  6666  mptfnf  6674  fnopabg  6676  mpteqb  7013  eqfnfv3  7031  fvn0ssdmfun  7073  caoftrn  7725  poseq  8160  wfr3g  8322  iiner  8793  ixpeq2  8915  ixpin  8927  ixpfi2  9314  wemaplem2  9516  frr3g  9735  dfac5  10128  kmlem6  10155  eltsk2g  10751  intgru  10814  axgroth6  10828  fsequb  14029  rexanuz  15421  rexanre  15422  cau3lem  15430  rlimcn3  15665  o1of2  15688  o1rlimmul  15694  climbdd  15747  sqrt2irr  16327  gcdcllem1  16579  pc11  16962  prmreclem2  16999  catpropd  17787  issubc3  17928  fucinv  18055  ispos2  18393  issubg3  19255  issubg4  19256  pmtrdifwrdel2  19600  ringsrg  20426  iunocv  21881  cply1mul  22506  scmatf1  22738  cpmatsubgpmat  22927  tgval2  23163  1stcelcls  23669  ptclsg  23823  ptcnplem  23829  fbun  24048  txflf  24214  ucncn  24492  prdsmet  24578  metequiv  24717  metequiv2  24718  ncvsi  25361  iscau4  25489  cmetcaulem  25498  evthicc2  25670  ismbfcn  25839  mbfi1flimlem  25932  rolle  26200  itgsubst  26259  plydivex  26509  ulmcaulem  26608  ulmcau  26609  ulmbdd  26612  ulmcn  26613  mumullem2  27395  2sqlem6  27638  oldfib  28621  tgcgr4  28851  axpasch  29346  axeuclid  29368  axcontlem2  29370  axcontlem4  29372  axcontlem7  29375  vtxd0nedgb  29896  fusgrregdegfi  29977  rusgr1vtxlem  29995  uspgr2wlkeq  30053  wlkdlem4  30091  lfgriswlk  30098  frgrreg  30816  frgrregord013  30817  friendshipgt3  30820  ocsh  31706  spanuni  31967  riesz4i  32486  leopadd  32555  leoptri  32559  leoptr  32560  inpr0  32949  disjunsn  33010  voliune  34684  volfiniune  34685  eulerpartlemr  34829  eulerpartlemn  34836  nummin  35542  fmlasucdisj  35928  wzel  36351  neibastop1  36927  numiunnum  37038  phpreu  38312  ptrecube  38328  poimirlem23  38351  poimirlem27  38355  ovoliunnfl  38370  voliunnfl  38372  volsupnfl  38373  itg2addnc  38382  inixp  38437  rngoueqz  38649  intidl  38738  pclclN  40723  tendoeq2  41606  deg1gprod  42965  mzpincl  43523  lerabdioph  43590  ltrabdioph  43593  nerabdioph  43594  dvdsrabdioph  43595  dford3lem1  43811  gneispace  44918  ssrabf  45890  r19.28zf  45935  climxrre  46522  stoweidlem7  46779  stoweidlem54  46826  dirkercncflem3  46877  ply1mulgsumlem1  49223  ldepsnlinclem1  49342  ldepsnlinclem2  49343  iinxp  49666  nelsubc2  49904