Theorem r19.26 3123

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 3100	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3100	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 521	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 475	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3102	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 412	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

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

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 3078

This theorem is used by:  r19.26-3  3124  ralbiim  3125  2ralbiim  3142  r19.26-2  3148  r19.27v  3192  r19.28v  3194  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  6290  dfpo2  6299  fncnv  6613  fnres  6666  mptfnf  6674  fnopabg  6676  mpteqb  7013  eqfnfv3  7031  fvn0ssdmfun  7074  caoftrn  7734  poseq  8175  wfr3g  8337  iiner  8810  ixpeq2  8939  ixpin  8951  ixpfi2  9339  wemaplem2  9541  frr3g  9760  dfac5  10207  kmlem6  10234  eltsk2g  10836  intgru  10899  axgroth6  10913  fsequb  14118  rexanuz  15513  rexanre  15514  cau3lem  15522  rlimcn3  15757  o1of2  15780  o1rlimmul  15786  climbdd  15839  sqrt2irr  16417  gcdcllem1  16669  pc11  17058  prmreclem2  17095  catpropd  17883  issubc3  18024  fucinv  18151  ispos2  18489  issubg3  19355  issubg4  19356  pmtrdifwrdel2  19700  dfring3  20518  ringsrg  20528  iunocv  21987  cply1mul  22614  scmatf1  22846  cpmatsubgpmat  23038  tgval2  23274  1stcelcls  23780  ptclsg  23934  ptcnplem  23940  fbun  24159  txflf  24325  ucncn  24603  prdsmet  24689  metequiv  24828  metequiv2  24829  ncvsi  25472  iscau4  25600  cmetcaulem  25609  evthicc2  25781  ismbfcn  25950  mbfi1flimlem  26043  rolle  26310  itgsubst  26369  plydivex  26618  ulmcaulem  26721  ulmcau  26722  ulmbdd  26725  ulmcn  26726  mumullem2  27507  2sqlem6  27750  oldfib  28763  tgcgr4  28994  axpasch  29519  axeuclid  29541  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  vtxd0nedgb  30069  fusgrregdegfi  30150  rusgr1vtxlem  30168  uspgr2wlkeq  30226  wlkdlem4  30264  lfgriswlk  30271  frgrreg  30995  frgrregord013  30996  friendshipgt3  30999  ocsh  31885  spanuni  32146  riesz4i  32665  leopadd  32734  leoptri  32738  leoptr  32739  inpr0  33128  disjunsn  33188  voliune  34862  volfiniune  34863  eulerpartlemr  35006  eulerpartlemn  35013  nummin  35722  fmlasucdisj  36164  wzel  36586  neibastop1  37147  numiunnum  37258  phpreu  38527  ptrecube  38538  poimirlem23  38561  poimirlem27  38565  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  itg2addnc  38592  inixp  38662  rngoueqz  38874  intidl  38963  pclclN  40948  tendoeq2  41831  deg1gprod  43190  mzpincl  43744  lerabdioph  43811  ltrabdioph  43814  nerabdioph  43815  dvdsrabdioph  43816  dford3lem1  44032  gneispace  45133  ssrabf  46128  r19.28zf  46173  climxrre  46759  stoweidlem7  47016  stoweidlem54  47063  dirkercncflem3  47114  ply1mulgsumlem1  49497  ldepsnlinclem1  49616  ldepsnlinclem2  49617  iinxp  49940  nelsubc2  50176