Theorem r19.26 3089

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  r19.26-3  3090  ralbiim  3091  2ralbiim  3108  r19.26-2  3114  r19.27v  3158  r19.28v  3160  reu8  3693  ssrab  4024  r19.28z  4449  r19.27z  4456  ralf0  4465  ralnralall  4466  2reu4lem  4473  2ralunsn  4846  iuneq2  4961  disjxun  5090  triin  5215  asymref2  6066  cnvpo  6235  dfpo2  6244  fncnv  6555  fnres  6609  mptfnf  6617  fnopabg  6619  mpteqb  6949  eqfnfv3  6967  fvn0ssdmfun  7008  caoftrn  7654  poseq  8091  wfr3g  8252  iiner  8716  ixpeq2  8838  ixpin  8850  ixpfi2  9240  wemaplem2  9439  frr3g  9652  dfac5  10023  kmlem6  10050  eltsk2g  10645  intgru  10708  axgroth6  10722  fsequb  13882  rexanuz  15253  rexanre  15254  cau3lem  15262  rlimcn3  15497  o1of2  15520  o1rlimmul  15526  climbdd  15579  sqrt2irr  16158  gcdcllem1  16410  pc11  16792  prmreclem2  16829  catpropd  17615  issubc3  17756  fucinv  17883  ispos2  18221  issubg3  19023  issubg4  19024  pmtrdifwrdel2  19365  ringsrg  20182  iunocv  21588  cply1mul  22181  scmatf1  22416  cpmatsubgpmat  22605  tgval2  22841  1stcelcls  23346  ptclsg  23500  ptcnplem  23506  fbun  23725  txflf  23891  ucncn  24170  prdsmet  24256  metequiv  24395  metequiv2  24396  ncvsi  25049  iscau4  25177  cmetcaulem  25186  evthicc2  25359  ismbfcn  25528  mbfi1flimlem  25621  rolle  25892  itgsubst  25954  plydivex  26203  ulmcaulem  26301  ulmcau  26302  ulmbdd  26305  ulmcn  26306  mumullem2  27088  2sqlem6  27332  tgcgr4  28476  axpasch  28886  axeuclid  28908  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  vtxd0nedgb  29434  fusgrregdegfi  29515  rusgr1vtxlem  29533  uspgr2wlkeq  29591  wlkdlem4  29629  lfgriswlk  29632  frgrreg  30338  frgrregord013  30339  friendshipgt3  30342  ocsh  31227  spanuni  31488  riesz4i  32007  leopadd  32076  leoptri  32080  leoptr  32081  inpr0  32476  disjunsn  32538  voliune  34196  volfiniune  34197  eulerpartlemr  34342  eulerpartlemn  34349  nummin  35058  fmlasucdisj  35372  wzel  35798  neibastop1  36333  numiunnum  36444  phpreu  37584  ptrecube  37600  poimirlem23  37623  poimirlem27  37627  ovoliunnfl  37642  voliunnfl  37644  volsupnfl  37645  itg2addnc  37654  inixp  37708  rngoueqz  37920  intidl  38009  pclclN  39870  tendoeq2  40753  deg1gprod  42113  mzpincl  42707  lerabdioph  42778  ltrabdioph  42781  nerabdioph  42782  dvdsrabdioph  42783  dford3lem1  42999  gneispace  44107  ssrabf  45092  r19.28zf  45137  climxrre  45731  stoweidlem7  45988  stoweidlem54  46035  dirkercncflem3  46086  ply1mulgsumlem1  48371  ldepsnlinclem1  48490  ldepsnlinclem2  48491  iinxp  48815  nelsubc2  49054