Theorem r19.26 3091

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  3092  ralbiim  3093  2ralbiim  3112  r19.26-2  3118  r19.27v  3164  r19.28v  3166  reu8  3701  ssrab  4032  r19.28z  4457  r19.27z  4464  ralf0  4473  ralnralall  4474  2reu4lem  4481  2ralunsn  4855  iuneq2  4971  disjxun  5100  triin  5226  asymref2  6078  cnvpo  6248  dfpo2  6257  fncnv  6573  fnres  6627  mptfnf  6635  fnopabg  6637  mpteqb  6969  eqfnfv3  6987  fvn0ssdmfun  7028  caoftrn  7674  poseq  8114  wfr3g  8275  iiner  8739  ixpeq2  8861  ixpin  8873  ixpfi2  9277  wemaplem2  9476  frr3g  9685  dfac5  10058  kmlem6  10085  eltsk2g  10680  intgru  10743  axgroth6  10757  fsequb  13916  rexanuz  15288  rexanre  15289  cau3lem  15297  rlimcn3  15532  o1of2  15555  o1rlimmul  15561  climbdd  15614  sqrt2irr  16193  gcdcllem1  16445  pc11  16827  prmreclem2  16864  catpropd  17650  issubc3  17791  fucinv  17918  ispos2  18256  issubg3  19058  issubg4  19059  pmtrdifwrdel2  19400  ringsrg  20217  iunocv  21623  cply1mul  22216  scmatf1  22451  cpmatsubgpmat  22640  tgval2  22876  1stcelcls  23381  ptclsg  23535  ptcnplem  23541  fbun  23760  txflf  23926  ucncn  24205  prdsmet  24291  metequiv  24430  metequiv2  24431  ncvsi  25084  iscau4  25212  cmetcaulem  25221  evthicc2  25394  ismbfcn  25563  mbfi1flimlem  25656  rolle  25927  itgsubst  25989  plydivex  26238  ulmcaulem  26336  ulmcau  26337  ulmbdd  26340  ulmcn  26341  mumullem2  27123  2sqlem6  27367  tgcgr4  28511  axpasch  28921  axeuclid  28943  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  vtxd0nedgb  29469  fusgrregdegfi  29550  rusgr1vtxlem  29568  uspgr2wlkeq  29626  wlkdlem4  29664  lfgriswlk  29667  frgrreg  30373  frgrregord013  30374  friendshipgt3  30377  ocsh  31262  spanuni  31523  riesz4i  32042  leopadd  32111  leoptri  32115  leoptr  32116  inpr0  32511  disjunsn  32573  voliune  34212  volfiniune  34213  eulerpartlemr  34358  eulerpartlemn  34365  nummin  35074  fmlasucdisj  35379  wzel  35805  neibastop1  36340  numiunnum  36451  phpreu  37591  ptrecube  37607  poimirlem23  37630  poimirlem27  37634  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  itg2addnc  37661  inixp  37715  rngoueqz  37927  intidl  38016  pclclN  39878  tendoeq2  40761  deg1gprod  42121  mzpincl  42715  lerabdioph  42786  ltrabdioph  42789  nerabdioph  42790  dvdsrabdioph  42791  dford3lem1  43008  gneispace  44116  ssrabf  45101  r19.28zf  45146  climxrre  45741  stoweidlem7  45998  stoweidlem54  46045  dirkercncflem3  46096  ply1mulgsumlem1  48368  ldepsnlinclem1  48487  ldepsnlinclem2  48488  iinxp  48812  nelsubc2  49051