Theorem r19.26 3137

Description: Restricted quantifier version of 19.26 1871. (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 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3128	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3128	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 515	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 473	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3124	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 410	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∀wral 3106

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  r19.26-2  3138  r19.26-3  3139  ralbiim  3141  r19.27v  3151  r19.28v  3152  reu8  3672  ssrab  4000  r19.28z  4401  r19.27z  4408  ralnralall  4416  2reu4lem  4423  2ralunsn  4787  iuneq2  4900  disjxun  5028  triin  5151  asymref2  5944  cnvpo  6106  fncnv  6397  fnres  6446  mptfnf  6455  fnopabg  6457  mpteqb  6764  eqfnfv3  6781  fvn0ssdmfun  6819  caoftrn  7424  wfr3g  7936  iiner  8352  ixpeq2  8458  ixpin  8470  ixpfi2  8806  wemaplem2  8995  dfac5  9539  kmlem6  9566  eltsk2g  10162  intgru  10225  axgroth6  10239  fsequb  13338  rexanuz  14697  rexanre  14698  cau3lem  14706  rlimcn2  14939  o1of2  14961  o1rlimmul  14967  climbdd  15020  sqrt2irr  15594  gcdcllem1  15838  pc11  16206  prmreclem2  16243  catpropd  16971  issubc3  17111  fucinv  17235  ispos2  17550  issubg3  18289  issubg4  18290  pmtrdifwrdel2  18606  ringsrg  19335  iunocv  20370  cply1mul  20923  scmatf1  21136  cpmatsubgpmat  21325  tgval2  21561  1stcelcls  22066  ptclsg  22220  ptcnplem  22226  fbun  22445  txflf  22611  ucncn  22891  prdsmet  22977  metequiv  23116  metequiv2  23117  ncvsi  23756  iscau4  23883  cmetcaulem  23892  evthicc2  24064  ismbfcn  24233  mbfi1flimlem  24326  rolle  24593  itgsubst  24652  plydivex  24893  ulmcaulem  24989  ulmcau  24990  ulmbdd  24993  ulmcn  24994  mumullem2  25765  2sqlem6  26007  tgcgr4  26325  axpasch  26735  axeuclid  26757  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  vtxd0nedgb  27278  fusgrregdegfi  27359  rusgr1vtxlem  27377  uspgr2wlkeq  27435  wlkdlem4  27475  lfgriswlk  27478  frgrreg  28179  frgrregord013  28180  friendshipgt3  28183  ocsh  29066  spanuni  29327  riesz4i  29846  leopadd  29915  leoptri  29919  leoptr  29920  inpr0  30304  disjunsn  30357  voliune  31598  volfiniune  31599  eulerpartlemr  31742  eulerpartlemn  31749  nummin  32474  fmlasucdisj  32759  dfpo2  33104  poseq  33208  wzel  33224  frr3g  33234  ssltun2  33383  neibastop1  33820  phpreu  35041  ptrecube  35057  poimirlem23  35080  poimirlem27  35084  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  itg2addnc  35111  inixp  35166  rngoueqz  35378  intidl  35467  pclclN  37187  tendoeq2  38070  mzpincl  39675  lerabdioph  39746  ltrabdioph  39749  nerabdioph  39750  dvdsrabdioph  39751  dford3lem1  39967  gneispace  40837  ssrabf  41750  climxrre  42392  stoweidlem7  42649  stoweidlem54  42696  dirkercncflem3  42747  2ralbiim  43660  ply1mulgsumlem1  44794  ldepsnlinclem1  44914  ldepsnlinclem2  44915