Theorem r19.26 3098

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

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

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 3052

This theorem is referenced by:  r19.26-3  3099  ralbiim  3100  2ralbiim  3119  r19.26-2  3125  r19.27v  3173  r19.28v  3175  reu8  3716  ssrab  4048  r19.28z  4473  r19.27z  4480  ralf0  4489  ralnralall  4490  2reu4lem  4497  2ralunsn  4871  iuneq2  4987  disjxun  5117  triin  5246  asymref2  6106  cnvpo  6276  dfpo2  6285  fncnv  6608  fnres  6664  mptfnf  6672  fnopabg  6674  mpteqb  7004  eqfnfv3  7022  fvn0ssdmfun  7063  caoftrn  7710  poseq  8155  wfr3g  8319  iiner  8801  ixpeq2  8923  ixpin  8935  ixpfi2  9360  wemaplem2  9559  frr3g  9768  dfac5  10141  kmlem6  10168  eltsk2g  10763  intgru  10826  axgroth6  10840  fsequb  13991  rexanuz  15362  rexanre  15363  cau3lem  15371  rlimcn3  15604  o1of2  15627  o1rlimmul  15633  climbdd  15686  sqrt2irr  16265  gcdcllem1  16516  pc11  16898  prmreclem2  16935  catpropd  17719  issubc3  17860  fucinv  17987  ispos2  18325  issubg3  19125  issubg4  19126  pmtrdifwrdel2  19465  ringsrg  20255  iunocv  21639  cply1mul  22232  scmatf1  22467  cpmatsubgpmat  22656  tgval2  22892  1stcelcls  23397  ptclsg  23551  ptcnplem  23557  fbun  23776  txflf  23942  ucncn  24221  prdsmet  24307  metequiv  24446  metequiv2  24447  ncvsi  25101  iscau4  25229  cmetcaulem  25238  evthicc2  25411  ismbfcn  25580  mbfi1flimlem  25673  rolle  25944  itgsubst  26006  plydivex  26255  ulmcaulem  26353  ulmcau  26354  ulmbdd  26357  ulmcn  26358  mumullem2  27140  2sqlem6  27384  tgcgr4  28456  axpasch  28866  axeuclid  28888  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  vtxd0nedgb  29414  fusgrregdegfi  29495  rusgr1vtxlem  29513  uspgr2wlkeq  29572  wlkdlem4  29611  lfgriswlk  29614  frgrreg  30321  frgrregord013  30322  friendshipgt3  30325  ocsh  31210  spanuni  31471  riesz4i  31990  leopadd  32059  leoptri  32063  leoptr  32064  inpr0  32459  disjunsn  32521  voliune  34206  volfiniune  34207  eulerpartlemr  34352  eulerpartlemn  34359  nummin  35068  fmlasucdisj  35367  wzel  35788  neibastop1  36323  numiunnum  36434  phpreu  37574  ptrecube  37590  poimirlem23  37613  poimirlem27  37617  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  itg2addnc  37644  inixp  37698  rngoueqz  37910  intidl  37999  pclclN  39856  tendoeq2  40739  deg1gprod  42099  mzpincl  42704  lerabdioph  42775  ltrabdioph  42778  nerabdioph  42779  dvdsrabdioph  42780  dford3lem1  42997  gneispace  44105  ssrabf  45086  r19.28zf  45131  climxrre  45727  stoweidlem7  45984  stoweidlem54  46031  dirkercncflem3  46082  ply1mulgsumlem1  48310  ldepsnlinclem1  48429  ldepsnlinclem2  48430  iinxp  48757  nelsubc2  48984