Theorem r19.26 3108

Description: Restricted quantifier version of 19.26 1867. (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 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 511	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 469	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3082	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 406	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3059

This theorem is referenced by:  r19.26-3  3109  ralbiim  3110  2ralbiim  3129  r19.26-2  3135  r19.27v  3185  r19.28v  3187  reu8  3741  ssrab  4082  r19.28z  4503  r19.27z  4510  ralf0  4519  ralnralall  4520  2reu4lem  4527  2ralunsn  4899  iuneq2  5015  disjxun  5145  triin  5281  asymref2  6139  cnvpo  6308  dfpo2  6317  fncnv  6640  fnres  6695  mptfnf  6703  fnopabg  6705  mpteqb  7034  eqfnfv3  7052  fvn0ssdmfun  7093  caoftrn  7736  poseq  8181  wfr3g  8345  iiner  8827  ixpeq2  8949  ixpin  8961  ixpfi2  9387  wemaplem2  9584  frr3g  9793  dfac5  10166  kmlem6  10193  eltsk2g  10788  intgru  10851  axgroth6  10865  fsequb  14012  rexanuz  15380  rexanre  15381  cau3lem  15389  rlimcn3  15622  o1of2  15645  o1rlimmul  15651  climbdd  15704  sqrt2irr  16281  gcdcllem1  16532  pc11  16913  prmreclem2  16950  catpropd  17753  issubc3  17899  fucinv  18029  ispos2  18372  issubg3  19174  issubg4  19175  pmtrdifwrdel2  19518  ringsrg  20310  iunocv  21716  cply1mul  22315  scmatf1  22552  cpmatsubgpmat  22741  tgval2  22978  1stcelcls  23484  ptclsg  23638  ptcnplem  23644  fbun  23863  txflf  24029  ucncn  24309  prdsmet  24395  metequiv  24537  metequiv2  24538  ncvsi  25198  iscau4  25326  cmetcaulem  25335  evthicc2  25508  ismbfcn  25677  mbfi1flimlem  25771  rolle  26042  itgsubst  26104  plydivex  26353  ulmcaulem  26451  ulmcau  26452  ulmbdd  26455  ulmcn  26456  mumullem2  27237  2sqlem6  27481  tgcgr4  28553  axpasch  28970  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  vtxd0nedgb  29520  fusgrregdegfi  29601  rusgr1vtxlem  29619  uspgr2wlkeq  29678  wlkdlem4  29717  lfgriswlk  29720  frgrreg  30422  frgrregord013  30423  friendshipgt3  30426  ocsh  31311  spanuni  31572  riesz4i  32091  leopadd  32160  leoptri  32164  leoptr  32165  inpr0  32557  disjunsn  32613  voliune  34209  volfiniune  34210  eulerpartlemr  34355  eulerpartlemn  34362  nummin  35083  fmlasucdisj  35383  wzel  35805  neibastop1  36341  numiunnum  36452  phpreu  37590  ptrecube  37606  poimirlem23  37629  poimirlem27  37633  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  itg2addnc  37660  inixp  37714  rngoueqz  37926  intidl  38015  pclclN  39873  tendoeq2  40756  deg1gprod  42121  mzpincl  42721  lerabdioph  42792  ltrabdioph  42795  nerabdioph  42796  dvdsrabdioph  42797  dford3lem1  43014  gneispace  44123  ssrabf  45053  r19.28zf  45101  climxrre  45705  stoweidlem7  45962  stoweidlem54  46009  dirkercncflem3  46060  ply1mulgsumlem1  48231  ldepsnlinclem1  48350  ldepsnlinclem2  48351