Theorem r19.26 3092

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 482	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3069	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3069	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 511	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 469	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3071	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 406	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

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

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 207  df-an 396  df-ral 3048

This theorem is referenced by:  r19.26-3  3093  ralbiim  3094  2ralbiim  3111  r19.26-2  3117  r19.27v  3161  r19.28v  3163  reu8  3687  ssrab  4018  r19.28z  4445  r19.27z  4452  ralf0  4461  ralnralall  4462  2reu4lem  4469  2ralunsn  4844  iuneq2  4959  disjxun  5087  triin  5212  asymref2  6063  cnvpo  6234  dfpo2  6243  fncnv  6554  fnres  6608  mptfnf  6616  fnopabg  6618  mpteqb  6948  eqfnfv3  6966  fvn0ssdmfun  7007  caoftrn  7651  poseq  8088  wfr3g  8249  iiner  8713  ixpeq2  8835  ixpin  8847  ixpfi2  9234  wemaplem2  9433  frr3g  9649  dfac5  10020  kmlem6  10047  eltsk2g  10642  intgru  10705  axgroth6  10719  fsequb  13882  rexanuz  15253  rexanre  15254  cau3lem  15262  rlimcn3  15497  o1of2  15520  o1rlimmul  15526  climbdd  15579  sqrt2irr  16158  gcdcllem1  16410  pc11  16792  prmreclem2  16829  catpropd  17615  issubc3  17756  fucinv  17883  ispos2  18221  issubg3  19057  issubg4  19058  pmtrdifwrdel2  19398  ringsrg  20215  iunocv  21618  cply1mul  22211  scmatf1  22446  cpmatsubgpmat  22635  tgval2  22871  1stcelcls  23376  ptclsg  23530  ptcnplem  23536  fbun  23755  txflf  23921  ucncn  24199  prdsmet  24285  metequiv  24424  metequiv2  24425  ncvsi  25078  iscau4  25206  cmetcaulem  25215  evthicc2  25388  ismbfcn  25557  mbfi1flimlem  25650  rolle  25921  itgsubst  25983  plydivex  26232  ulmcaulem  26330  ulmcau  26331  ulmbdd  26334  ulmcn  26335  mumullem2  27117  2sqlem6  27361  tgcgr4  28509  axpasch  28919  axeuclid  28941  axcontlem2  28943  axcontlem4  28945  axcontlem7  28948  vtxd0nedgb  29467  fusgrregdegfi  29548  rusgr1vtxlem  29566  uspgr2wlkeq  29624  wlkdlem4  29662  lfgriswlk  29665  frgrreg  30374  frgrregord013  30375  friendshipgt3  30378  ocsh  31263  spanuni  31524  riesz4i  32043  leopadd  32112  leoptri  32116  leoptr  32117  inpr0  32512  disjunsn  32574  voliune  34242  volfiniune  34243  eulerpartlemr  34387  eulerpartlemn  34394  nummin  35104  fmlasucdisj  35443  wzel  35866  neibastop1  36401  numiunnum  36512  phpreu  37652  ptrecube  37668  poimirlem23  37691  poimirlem27  37695  ovoliunnfl  37710  voliunnfl  37712  volsupnfl  37713  itg2addnc  37722  inixp  37776  rngoueqz  37988  intidl  38077  pclclN  39938  tendoeq2  40821  deg1gprod  42181  mzpincl  42775  lerabdioph  42846  ltrabdioph  42849  nerabdioph  42850  dvdsrabdioph  42851  dford3lem1  43067  gneispace  44175  ssrabf  45159  r19.28zf  45204  climxrre  45796  stoweidlem7  46053  stoweidlem54  46100  dirkercncflem3  46151  ply1mulgsumlem1  48426  ldepsnlinclem1  48545  ldepsnlinclem2  48546  iinxp  48870  nelsubc2  49109