Theorem r19.26 3125

Description: Restricted quantifier version of 19.26 1900. (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 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3102	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3102	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 520	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 474	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3104	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 411	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is referenced by:  r19.26-3  3126  ralbiim  3127  2ralbiim  3144  r19.26-2  3150  r19.27v  3194  r19.28v  3196  reu8  3696  ssrab  4025  r19.28z  4463  r19.27z  4471  ralnralall  4474  2reu4lem  4484  2ralunsn  4860  iuneq2  4976  disjxun  5107  triin  5235  asymref2  6117  cnvpo  6288  dfpo2  6297  fncnv  6609  fnres  6662  mptfnf  6670  fnopabg  6672  mpteqb  7009  eqfnfv3  7027  fvn0ssdmfun  7069  caoftrn  7715  poseq  8150  wfr3g  8312  iiner  8783  ixpeq2  8905  ixpin  8917  ixpfi2  9303  wemaplem2  9505  frr3g  9724  dfac5  10108  kmlem6  10135  eltsk2g  10731  intgru  10794  axgroth6  10808  fsequb  14007  rexanuz  15393  rexanre  15394  cau3lem  15402  rlimcn3  15637  o1of2  15660  o1rlimmul  15666  climbdd  15719  sqrt2irr  16300  gcdcllem1  16552  pc11  16935  prmreclem2  16972  catpropd  17760  issubc3  17901  fucinv  18028  ispos2  18366  issubg3  19206  issubg4  19207  pmtrdifwrdel2  19551  ringsrg  20376  iunocv  21831  cply1mul  22456  scmatf1  22688  cpmatsubgpmat  22877  tgval2  23113  1stcelcls  23618  ptclsg  23772  ptcnplem  23778  fbun  23997  txflf  24163  ucncn  24441  prdsmet  24527  metequiv  24666  metequiv2  24667  ncvsi  25310  iscau4  25438  cmetcaulem  25447  evthicc2  25619  ismbfcn  25788  mbfi1flimlem  25881  rolle  26149  itgsubst  26208  plydivex  26458  ulmcaulem  26557  ulmcau  26558  ulmbdd  26561  ulmcn  26562  mumullem2  27344  2sqlem6  27587  oldfib  28570  tgcgr4  28800  axpasch  29291  axeuclid  29313  axcontlem2  29315  axcontlem4  29317  axcontlem7  29320  vtxd0nedgb  29838  fusgrregdegfi  29919  rusgr1vtxlem  29937  uspgr2wlkeq  29995  wlkdlem4  30033  lfgriswlk  30036  frgrreg  30745  frgrregord013  30746  friendshipgt3  30749  ocsh  31635  spanuni  31896  riesz4i  32415  leopadd  32484  leoptri  32488  leoptr  32489  inpr0  32878  disjunsn  32939  voliune  34619  volfiniune  34620  eulerpartlemr  34764  eulerpartlemn  34771  nummin  35484  fmlasucdisj  35891  wzel  36314  neibastop1  36870  numiunnum  36981  phpreu  38255  ptrecube  38271  poimirlem23  38294  poimirlem27  38298  ovoliunnfl  38313  voliunnfl  38315  volsupnfl  38316  itg2addnc  38325  inixp  38379  rngoueqz  38591  intidl  38680  pclclN  40665  tendoeq2  41548  deg1gprod  42907  mzpincl  43465  lerabdioph  43532  ltrabdioph  43535  nerabdioph  43536  dvdsrabdioph  43537  dford3lem1  43753  gneispace  44860  ssrabf  45832  r19.28zf  45877  climxrre  46464  stoweidlem7  46721  stoweidlem54  46768  dirkercncflem3  46819  ply1mulgsumlem1  49166  ldepsnlinclem1  49285  ldepsnlinclem2  49286  iinxp  49609  nelsubc2  49847