Theorem r19.26 3131

Description: Restricted quantifier version of 19.26 1897. (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 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 520	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 474	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 411	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  r19.26-3  3132  ralbiim  3133  2ralbiim  3150  r19.26-2  3156  r19.27v  3200  r19.28v  3202  reu8  3705  ssrab  4033  r19.28z  4468  r19.27z  4476  ralnralall  4479  2reu4lem  4489  2ralunsn  4864  iuneq2  4980  disjxun  5111  triin  5239  asymref2  6118  cnvpo  6289  dfpo2  6298  fncnv  6610  fnres  6663  mptfnf  6671  fnopabg  6673  mpteqb  7010  eqfnfv3  7028  fvn0ssdmfun  7070  caoftrn  7716  poseq  8153  wfr3g  8315  iiner  8786  ixpeq2  8908  ixpin  8920  ixpfi2  9306  wemaplem2  9508  frr3g  9727  dfac5  10111  kmlem6  10138  eltsk2g  10735  intgru  10798  axgroth6  10812  fsequb  14010  rexanuz  15396  rexanre  15397  cau3lem  15405  rlimcn3  15640  o1of2  15663  o1rlimmul  15669  climbdd  15722  sqrt2irr  16304  gcdcllem1  16556  pc11  16939  prmreclem2  16976  catpropd  17764  issubc3  17905  fucinv  18032  ispos2  18370  issubg3  19210  issubg4  19211  pmtrdifwrdel2  19555  ringsrg  20379  iunocv  21799  cply1mul  22424  scmatf1  22656  cpmatsubgpmat  22845  tgval2  23081  1stcelcls  23586  ptclsg  23740  ptcnplem  23746  fbun  23965  txflf  24131  ucncn  24409  prdsmet  24495  metequiv  24634  metequiv2  24635  ncvsi  25278  iscau4  25406  cmetcaulem  25415  evthicc2  25587  ismbfcn  25756  mbfi1flimlem  25849  rolle  26117  itgsubst  26176  plydivex  26426  ulmcaulem  26522  ulmcau  26523  ulmbdd  26526  ulmcn  26527  mumullem2  27309  2sqlem6  27552  oldfib  28535  tgcgr4  28765  axpasch  29231  axeuclid  29253  axcontlem2  29255  axcontlem4  29257  axcontlem7  29260  vtxd0nedgb  29778  fusgrregdegfi  29859  rusgr1vtxlem  29877  uspgr2wlkeq  29935  wlkdlem4  29973  lfgriswlk  29976  frgrreg  30685  frgrregord013  30686  friendshipgt3  30689  ocsh  31575  spanuni  31836  riesz4i  32355  leopadd  32424  leoptri  32428  leoptr  32429  inpr0  32818  disjunsn  32879  voliune  34563  volfiniune  34564  eulerpartlemr  34708  eulerpartlemn  34715  nummin  35426  fmlasucdisj  35789  wzel  36212  neibastop1  36758  numiunnum  36869  phpreu  38142  ptrecube  38158  poimirlem23  38181  poimirlem27  38185  ovoliunnfl  38200  voliunnfl  38202  volsupnfl  38203  itg2addnc  38212  inixp  38266  rngoueqz  38478  intidl  38567  pclclN  40554  tendoeq2  41437  deg1gprod  42796  mzpincl  43356  lerabdioph  43423  ltrabdioph  43426  nerabdioph  43427  dvdsrabdioph  43428  dford3lem1  43644  gneispace  44751  ssrabf  45723  r19.28zf  45768  climxrre  46355  stoweidlem7  46612  stoweidlem54  46659  dirkercncflem3  46710  ply1mulgsumlem1  49050  ldepsnlinclem1  49169  ldepsnlinclem2  49170  iinxp  49493  nelsubc2  49731