Theorem r19.26 3097

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

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

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

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

This theorem is referenced by:  r19.26-3  3098  ralbiim  3099  2ralbiim  3116  r19.26-2  3122  r19.27v  3166  r19.28v  3168  reu8  3679  ssrab  4011  r19.28z  4442  r19.27z  4450  ralnralall  4453  2reu4lem  4463  2ralunsn  4838  iuneq2  4953  disjxun  5083  triin  5209  asymref2  6080  cnvpo  6251  dfpo2  6260  fncnv  6571  fnres  6625  mptfnf  6633  fnopabg  6635  mpteqb  6967  eqfnfv3  6985  fvn0ssdmfun  7026  caoftrn  7672  poseq  8108  wfr3g  8269  iiner  8736  ixpeq2  8859  ixpin  8871  ixpfi2  9260  wemaplem2  9462  frr3g  9680  dfac5  10051  kmlem6  10078  eltsk2g  10674  intgru  10737  axgroth6  10751  fsequb  13937  rexanuz  15308  rexanre  15309  cau3lem  15317  rlimcn3  15552  o1of2  15575  o1rlimmul  15581  climbdd  15634  sqrt2irr  16216  gcdcllem1  16468  pc11  16851  prmreclem2  16888  catpropd  17675  issubc3  17816  fucinv  17943  ispos2  18281  issubg3  19120  issubg4  19121  pmtrdifwrdel2  19461  ringsrg  20278  iunocv  21661  cply1mul  22261  scmatf1  22496  cpmatsubgpmat  22685  tgval2  22921  1stcelcls  23426  ptclsg  23580  ptcnplem  23586  fbun  23805  txflf  23971  ucncn  24249  prdsmet  24335  metequiv  24474  metequiv2  24475  ncvsi  25118  iscau4  25246  cmetcaulem  25255  evthicc2  25427  ismbfcn  25596  mbfi1flimlem  25689  rolle  25957  itgsubst  26016  plydivex  26263  ulmcaulem  26359  ulmcau  26360  ulmbdd  26363  ulmcn  26364  mumullem2  27143  2sqlem6  27386  oldfib  28369  tgcgr4  28599  axpasch  29010  axeuclid  29032  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  vtxd0nedgb  29557  fusgrregdegfi  29638  rusgr1vtxlem  29656  uspgr2wlkeq  29714  wlkdlem4  29752  lfgriswlk  29755  frgrreg  30464  frgrregord013  30465  friendshipgt3  30468  ocsh  31354  spanuni  31615  riesz4i  32134  leopadd  32203  leoptri  32207  leoptr  32208  inpr0  32602  disjunsn  32664  voliune  34373  volfiniune  34374  eulerpartlemr  34518  eulerpartlemn  34525  nummin  35236  fmlasucdisj  35581  wzel  36004  neibastop1  36541  numiunnum  36652  phpreu  37925  ptrecube  37941  poimirlem23  37964  poimirlem27  37968  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnc  37995  inixp  38049  rngoueqz  38261  intidl  38350  pclclN  40337  tendoeq2  41220  deg1gprod  42579  mzpincl  43166  lerabdioph  43233  ltrabdioph  43236  nerabdioph  43237  dvdsrabdioph  43238  dford3lem1  43454  gneispace  44561  ssrabf  45544  r19.28zf  45589  climxrre  46178  stoweidlem7  46435  stoweidlem54  46482  dirkercncflem3  46533  ply1mulgsumlem1  48862  ldepsnlinclem1  48981  ldepsnlinclem2  48982  iinxp  49306  nelsubc2  49544