Theorem r19.26 3098

Description: Restricted quantifier version of 19.26 1872. (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 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 511	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 469	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3077	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 406	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

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

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

This theorem is referenced by:  r19.26-3  3099  ralbiim  3100  2ralbiim  3117  r19.26-2  3123  r19.27v  3167  r19.28v  3169  reu8  3693  ssrab  4025  r19.28z  4457  r19.27z  4465  ralnralall  4468  2reu4lem  4478  2ralunsn  4853  iuneq2  4968  disjxun  5098  triin  5223  asymref2  6082  cnvpo  6253  dfpo2  6262  fncnv  6573  fnres  6627  mptfnf  6635  fnopabg  6637  mpteqb  6969  eqfnfv3  6987  fvn0ssdmfun  7028  caoftrn  7673  poseq  8110  wfr3g  8271  iiner  8738  ixpeq2  8861  ixpin  8873  ixpfi2  9262  wemaplem2  9464  frr3g  9680  dfac5  10051  kmlem6  10078  eltsk2g  10674  intgru  10737  axgroth6  10751  fsequb  13910  rexanuz  15281  rexanre  15282  cau3lem  15290  rlimcn3  15525  o1of2  15548  o1rlimmul  15554  climbdd  15607  sqrt2irr  16186  gcdcllem1  16438  pc11  16820  prmreclem2  16857  catpropd  17644  issubc3  17785  fucinv  17912  ispos2  18250  issubg3  19086  issubg4  19087  pmtrdifwrdel2  19427  ringsrg  20244  iunocv  21648  cply1mul  22252  scmatf1  22487  cpmatsubgpmat  22676  tgval2  22912  1stcelcls  23417  ptclsg  23571  ptcnplem  23577  fbun  23796  txflf  23962  ucncn  24240  prdsmet  24326  metequiv  24465  metequiv2  24466  ncvsi  25119  iscau4  25247  cmetcaulem  25256  evthicc2  25429  ismbfcn  25598  mbfi1flimlem  25691  rolle  25962  itgsubst  26024  plydivex  26273  ulmcaulem  26371  ulmcau  26372  ulmbdd  26375  ulmcn  26376  mumullem2  27158  2sqlem6  27402  oldfib  28385  tgcgr4  28615  axpasch  29026  axeuclid  29048  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  vtxd0nedgb  29574  fusgrregdegfi  29655  rusgr1vtxlem  29673  uspgr2wlkeq  29731  wlkdlem4  29769  lfgriswlk  29772  frgrreg  30481  frgrregord013  30482  friendshipgt3  30485  ocsh  31371  spanuni  31632  riesz4i  32151  leopadd  32220  leoptri  32224  leoptr  32225  inpr0  32619  disjunsn  32681  voliune  34407  volfiniune  34408  eulerpartlemr  34552  eulerpartlemn  34559  nummin  35270  fmlasucdisj  35615  wzel  36038  neibastop1  36575  numiunnum  36686  phpreu  37855  ptrecube  37871  poimirlem23  37894  poimirlem27  37898  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  itg2addnc  37925  inixp  37979  rngoueqz  38191  intidl  38280  pclclN  40267  tendoeq2  41150  deg1gprod  42510  mzpincl  43091  lerabdioph  43162  ltrabdioph  43165  nerabdioph  43166  dvdsrabdioph  43167  dford3lem1  43383  gneispace  44490  ssrabf  45473  r19.28zf  45518  climxrre  46108  stoweidlem7  46365  stoweidlem54  46412  dirkercncflem3  46463  ply1mulgsumlem1  48746  ldepsnlinclem1  48865  ldepsnlinclem2  48866  iinxp  49190  nelsubc2  49428