Theorem r19.26 3122

Description: Restricted quantifier version of 19.26 1903. (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 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 521	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 475	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3101	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 412	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  r19.26-3  3123  ralbiim  3124  2ralbiim  3141  r19.26-2  3147  r19.27v  3191  r19.28v  3193  reu8  3691  ssrab  4019  r19.28z  4458  r19.27z  4466  ralnralall  4469  2reu4lem  4479  2ralunsn  4855  iuneq2  4971  disjxun  5101  triin  5229  asymref2  6111  cnvpo  6285  dfpo2  6294  fncnv  6607  fnres  6660  mptfnf  6668  fnopabg  6670  mpteqb  7007  eqfnfv3  7025  fvn0ssdmfun  7068  caoftrn  7720  poseq  8157  wfr3g  8319  iiner  8790  ixpeq2  8919  ixpin  8931  ixpfi2  9318  wemaplem2  9520  frr3g  9739  dfac5  10132  kmlem6  10159  eltsk2g  10761  intgru  10824  axgroth6  10838  fsequb  14040  rexanuz  15434  rexanre  15435  cau3lem  15443  rlimcn3  15678  o1of2  15701  o1rlimmul  15707  climbdd  15760  sqrt2irr  16338  gcdcllem1  16590  pc11  16973  prmreclem2  17010  catpropd  17798  issubc3  17939  fucinv  18066  ispos2  18404  issubg3  19269  issubg4  19270  pmtrdifwrdel2  19614  ringsrg  20440  iunocv  21895  cply1mul  22522  scmatf1  22754  cpmatsubgpmat  22946  tgval2  23182  1stcelcls  23688  ptclsg  23842  ptcnplem  23848  fbun  24067  txflf  24233  ucncn  24511  prdsmet  24597  metequiv  24736  metequiv2  24737  ncvsi  25380  iscau4  25508  cmetcaulem  25517  evthicc2  25689  ismbfcn  25858  mbfi1flimlem  25951  rolle  26218  itgsubst  26277  plydivex  26528  ulmcaulem  26631  ulmcau  26632  ulmbdd  26635  ulmcn  26636  mumullem2  27417  2sqlem6  27660  oldfib  28643  tgcgr4  28874  axpasch  29399  axeuclid  29421  axcontlem2  29423  axcontlem4  29425  axcontlem7  29428  vtxd0nedgb  29949  fusgrregdegfi  30030  rusgr1vtxlem  30048  uspgr2wlkeq  30106  wlkdlem4  30144  lfgriswlk  30151  frgrreg  30875  frgrregord013  30876  friendshipgt3  30879  ocsh  31765  spanuni  32026  riesz4i  32545  leopadd  32614  leoptri  32618  leoptr  32619  inpr0  33008  disjunsn  33068  voliune  34741  volfiniune  34742  eulerpartlemr  34886  eulerpartlemn  34893  nummin  35599  fmlasucdisj  35979  wzel  36402  neibastop1  36979  numiunnum  37090  phpreu  38359  ptrecube  38370  poimirlem23  38393  poimirlem27  38397  ovoliunnfl  38412  voliunnfl  38414  volsupnfl  38415  itg2addnc  38424  inixp  38479  rngoueqz  38691  intidl  38780  pclclN  40765  tendoeq2  41648  deg1gprod  43007  mzpincl  43580  lerabdioph  43647  ltrabdioph  43650  nerabdioph  43651  dvdsrabdioph  43652  dford3lem1  43868  gneispace  44975  ssrabf  45947  r19.28zf  45992  climxrre  46579  stoweidlem7  46836  stoweidlem54  46883  dirkercncflem3  46934  ply1mulgsumlem1  49317  ldepsnlinclem1  49436  ldepsnlinclem2  49437  iinxp  49760  nelsubc2  49996