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  3680  ssrab  4012  r19.28z  4443  r19.27z  4451  ralnralall  4454  2reu4lem  4464  2ralunsn  4839  iuneq2  4954  disjxun  5084  triin  5210  asymref2  6075  cnvpo  6246  dfpo2  6255  fncnv  6566  fnres  6620  mptfnf  6628  fnopabg  6630  mpteqb  6962  eqfnfv3  6980  fvn0ssdmfun  7021  caoftrn  7666  poseq  8102  wfr3g  8263  iiner  8730  ixpeq2  8853  ixpin  8865  ixpfi2  9254  wemaplem2  9456  frr3g  9674  dfac5  10045  kmlem6  10072  eltsk2g  10668  intgru  10731  axgroth6  10745  fsequb  13931  rexanuz  15302  rexanre  15303  cau3lem  15311  rlimcn3  15546  o1of2  15569  o1rlimmul  15575  climbdd  15628  sqrt2irr  16210  gcdcllem1  16462  pc11  16845  prmreclem2  16882  catpropd  17669  issubc3  17810  fucinv  17937  ispos2  18275  issubg3  19114  issubg4  19115  pmtrdifwrdel2  19455  ringsrg  20272  iunocv  21674  cply1mul  22274  scmatf1  22509  cpmatsubgpmat  22698  tgval2  22934  1stcelcls  23439  ptclsg  23593  ptcnplem  23599  fbun  23818  txflf  23984  ucncn  24262  prdsmet  24348  metequiv  24487  metequiv2  24488  ncvsi  25131  iscau4  25259  cmetcaulem  25268  evthicc2  25440  ismbfcn  25609  mbfi1flimlem  25702  rolle  25970  itgsubst  26029  plydivex  26277  ulmcaulem  26375  ulmcau  26376  ulmbdd  26379  ulmcn  26380  mumullem2  27160  2sqlem6  27403  oldfib  28386  tgcgr4  28616  axpasch  29027  axeuclid  29049  axcontlem2  29051  axcontlem4  29053  axcontlem7  29056  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  32682  voliune  34392  volfiniune  34393  eulerpartlemr  34537  eulerpartlemn  34544  nummin  35255  fmlasucdisj  35600  wzel  36023  neibastop1  36560  numiunnum  36671  phpreu  37942  ptrecube  37958  poimirlem23  37981  poimirlem27  37985  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  itg2addnc  38012  inixp  38066  rngoueqz  38278  intidl  38367  pclclN  40354  tendoeq2  41237  deg1gprod  42596  mzpincl  43183  lerabdioph  43254  ltrabdioph  43257  nerabdioph  43258  dvdsrabdioph  43259  dford3lem1  43475  gneispace  44582  ssrabf  45565  r19.28zf  45610  climxrre  46199  stoweidlem7  46456  stoweidlem54  46503  dirkercncflem3  46554  ply1mulgsumlem1  48877  ldepsnlinclem1  48996  ldepsnlinclem2  48997  iinxp  49321  nelsubc2  49559