Theorem r19.26 3109

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 481	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 483	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 510	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 468	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 405	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394  ∀wral 3059

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 206  df-an 395  df-ral 3060

This theorem is referenced by:  r19.26-3  3110  ralbiim  3111  2ralbiim  3130  r19.26-2  3136  r19.27v  3185  r19.28v  3187  reu8  3728  ssrab  4069  r19.28z  4496  r19.27z  4503  ralf0  4512  ralnralall  4517  2reu4lem  4524  2ralunsn  4894  iuneq2  5015  disjxun  5145  triin  5281  asymref2  6117  cnvpo  6285  dfpo2  6294  fncnv  6620  fnres  6676  mptfnf  6684  fnopabg  6686  mpteqb  7016  eqfnfv3  7033  fvn0ssdmfun  7075  caoftrn  7710  poseq  8146  wfr3g  8309  iiner  8785  ixpeq2  8907  ixpin  8919  ixpfi2  9352  wemaplem2  9544  frr3g  9753  dfac5  10125  kmlem6  10152  eltsk2g  10748  intgru  10811  axgroth6  10825  fsequb  13944  rexanuz  15296  rexanre  15297  cau3lem  15305  rlimcn3  15538  o1of2  15561  o1rlimmul  15567  climbdd  15622  sqrt2irr  16196  gcdcllem1  16444  pc11  16817  prmreclem2  16854  catpropd  17657  issubc3  17803  fucinv  17930  ispos2  18272  issubg3  19060  issubg4  19061  pmtrdifwrdel2  19395  ringsrg  20185  iunocv  21453  cply1mul  22038  scmatf1  22253  cpmatsubgpmat  22442  tgval2  22679  1stcelcls  23185  ptclsg  23339  ptcnplem  23345  fbun  23564  txflf  23730  ucncn  24010  prdsmet  24096  metequiv  24238  metequiv2  24239  ncvsi  24899  iscau4  25027  cmetcaulem  25036  evthicc2  25209  ismbfcn  25378  mbfi1flimlem  25472  rolle  25742  itgsubst  25801  plydivex  26046  ulmcaulem  26142  ulmcau  26143  ulmbdd  26146  ulmcn  26147  mumullem2  26920  2sqlem6  27162  tgcgr4  28049  axpasch  28466  axeuclid  28488  axcontlem2  28490  axcontlem4  28492  axcontlem7  28495  vtxd0nedgb  29012  fusgrregdegfi  29093  rusgr1vtxlem  29111  uspgr2wlkeq  29170  wlkdlem4  29209  lfgriswlk  29212  frgrreg  29914  frgrregord013  29915  friendshipgt3  29918  ocsh  30803  spanuni  31064  riesz4i  31583  leopadd  31652  leoptri  31656  leoptr  31657  inpr0  32036  disjunsn  32092  voliune  33525  volfiniune  33526  eulerpartlemr  33671  eulerpartlemn  33678  nummin  34392  fmlasucdisj  34688  wzel  35100  neibastop1  35547  phpreu  36775  ptrecube  36791  poimirlem23  36814  poimirlem27  36818  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  itg2addnc  36845  inixp  36899  rngoueqz  37111  intidl  37200  pclclN  39065  tendoeq2  39948  mzpincl  41774  lerabdioph  41845  ltrabdioph  41848  nerabdioph  41849  dvdsrabdioph  41850  dford3lem1  42067  gneispace  43187  ssrabf  44104  r19.28zf  44154  climxrre  44764  stoweidlem7  45021  stoweidlem54  45068  dirkercncflem3  45119  ply1mulgsumlem1  47154  ldepsnlinclem1  47273  ldepsnlinclem2  47274