Theorem r19.26 3170

Description: Restricted quantifier version of 19.26 1871. (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 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3160	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3160	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 514	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 472	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3156	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 409	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 211	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∀wral 3138

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  r19.26-2  3171  r19.26-3  3172  ralbiim  3174  r19.27v  3184  r19.27vOLD  3185  r19.28v  3186  reu8  3724  ssrab  4049  r19.28z  4443  r19.27z  4450  ralnralall  4458  2reu4lem  4465  2ralunsn  4825  iuneq2  4938  disjxun  5064  triin  5187  asymref2  5977  cnvpo  6138  fncnv  6427  fnres  6474  mptfnf  6483  fnopabg  6485  mpteqb  6787  eqfnfv3  6804  fvn0ssdmfun  6842  caoftrn  7444  wfr3g  7953  iiner  8369  ixpeq2  8475  ixpin  8487  ixpfi2  8822  wemaplem2  9011  dfac5  9554  kmlem6  9581  eltsk2g  10173  intgru  10236  axgroth6  10250  fsequb  13344  rexanuz  14705  rexanre  14706  cau3lem  14714  rlimcn2  14947  o1of2  14969  o1rlimmul  14975  climbdd  15028  sqrt2irr  15602  gcdcllem1  15848  pc11  16216  prmreclem2  16253  catpropd  16979  issubc3  17119  fucinv  17243  ispos2  17558  issubg3  18297  issubg4  18298  pmtrdifwrdel2  18614  ringsrg  19339  cply1mul  20462  iunocv  20825  scmatf1  21140  cpmatsubgpmat  21328  tgval2  21564  1stcelcls  22069  ptclsg  22223  ptcnplem  22229  fbun  22448  txflf  22614  ucncn  22894  prdsmet  22980  metequiv  23119  metequiv2  23120  ncvsi  23755  iscau4  23882  cmetcaulem  23891  evthicc2  24061  ismbfcn  24230  mbfi1flimlem  24323  rolle  24587  itgsubst  24646  plydivex  24886  ulmcaulem  24982  ulmcau  24983  ulmbdd  24986  ulmcn  24987  mumullem2  25757  2sqlem6  25999  tgcgr4  26317  axpasch  26727  axeuclid  26749  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  vtxd0nedgb  27270  fusgrregdegfi  27351  rusgr1vtxlem  27369  uspgr2wlkeq  27427  wlkdlem4  27467  lfgriswlk  27470  frgrreg  28173  frgrregord013  28174  friendshipgt3  28177  ocsh  29060  spanuni  29321  riesz4i  29840  leopadd  29909  leoptri  29913  leoptr  29914  inpr0  30292  disjunsn  30344  voliune  31488  volfiniune  31489  eulerpartlemr  31632  eulerpartlemn  31639  fmlasucdisj  32646  dfpo2  32991  poseq  33095  wzel  33111  frr3g  33121  ssltun2  33270  neibastop1  33707  phpreu  34891  ptrecube  34907  poimirlem23  34930  poimirlem27  34934  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnc  34961  inixp  35018  rngoueqz  35233  intidl  35322  pclclN  37042  tendoeq2  37925  mzpincl  39351  lerabdioph  39422  ltrabdioph  39425  nerabdioph  39426  dvdsrabdioph  39427  dford3lem1  39643  gneispace  40504  ssrabf  41401  climxrre  42051  stoweidlem7  42312  stoweidlem54  42359  dirkercncflem3  42410  2ralbiim  43323  ply1mulgsumlem1  44460  ldepsnlinclem1  44580  ldepsnlinclem2  44581