Theorem r19.26 3126

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

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

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 3081

This theorem is used by:  r19.26-3  3127  ralbiim  3128  2ralbiim  3145  r19.26-2  3151  r19.27v  3195  r19.28v  3197  reu8  3694  ssrab  3999  r19.28z  4461  r19.27z  4469  ralnralall  4472  2reu4lem  4482  2ralunsn  4831  iuneq2  4976  disjxun  5106  triin  5235  asymref2  6129  cnvpo  6314  dfpo2  6325  fncnv  6643  fnres  6696  mptfnf  6704  fnopabg  6706  mpteqb  7044  eqfnfv3  7062  fvn0ssdmfun  7106  caoftrn  7766  poseq  8212  wfr3g  8375  iiner  8848  ixpeq2  8977  ixpin  8989  ixpfi2  9377  wemaplem2  9578  frr3g  9797  dfac5  10246  kmlem6  10273  eltsk2g  10875  intgru  10938  axgroth6  10952  fsequb  14158  rexanuz  15557  rexanre  15558  cau3lem  15566  rlimcn3  15801  o1of2  15824  o1rlimmul  15830  climbdd  15883  sqrt2irr  16461  gcdcllem1  16713  pc11  17102  prmreclem2  17139  catpropd  17933  issubc3  18074  fucinv  18201  ispos2  18539  issubg3  19405  issubg4  19406  pmtrdifwrdel2  19751  dfring3  20569  ringsrg  20579  iunocv  22042  cply1mul  22669  scmatf1  22901  cpmatsubgpmat  23093  tgval2  23329  1stcelcls  23835  ptclsg  23989  ptcnplem  23995  fbun  24214  txflf  24380  ucncn  24658  prdsmet  24744  metequiv  24883  metequiv2  24884  ncvsi  25527  iscau4  25655  cmetcaulem  25664  evthicc2  25836  ismbfcn  26005  mbfi1flimlem  26098  rolle  26365  itgsubst  26424  plydivex  26673  ulmcaulem  26778  ulmcau  26779  ulmbdd  26782  ulmcn  26783  mumullem2  27564  2sqlem6  27807  oldfib  28820  tgcgr4  29051  axpasch  29576  axeuclid  29598  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  vtxd0nedgb  30126  fusgrregdegfi  30207  rusgr1vtxlem  30225  uspgr2wlkeq  30283  wlkdlem4  30321  lfgriswlk  30328  frgrreg  31052  frgrregord013  31053  friendshipgt3  31056  ocsh  31942  spanuni  32203  riesz4i  32722  leopadd  32791  leoptri  32795  leoptr  32796  inpr0  33226  disjunsn  33286  voliune  34973  volfiniune  34974  eulerpartlemr  35117  eulerpartlemn  35124  nummin  35847  fmlasucdisj  36372  wzel  36801  neibastop1  37362  numiunnum  37473  phpreu  38795  ptrecube  38806  poimirlem23  38829  poimirlem27  38833  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  itg2addnc  38860  inixp  38930  rngoueqz  39140  intidl  39229  pclclN  41214  tendoeq2  42097  deg1gprod  43456  mzpincl  44011  lerabdioph  44078  ltrabdioph  44081  nerabdioph  44082  dvdsrabdioph  44083  dford3lem1  44299  gneispace  45395  ssrabf  46402  r19.28zf  46447  climxrre  47033  stoweidlem7  47290  stoweidlem54  47337  dirkercncflem3  47388  ply1mulgsumlem1  49829  ldepsnlinclem1  49948  ldepsnlinclem2  49949  iinxp  50273  nelsubc2  50514