Theorem r19.26 3108

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∀wral 3058

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3059

This theorem is referenced by:  r19.26-3  3109  ralbiim  3110  2ralbiim  3129  r19.26-2  3135  r19.27v  3184  r19.28v  3186  reu8  3728  ssrab  4068  r19.28z  4498  r19.27z  4505  ralf0  4514  ralnralall  4519  2reu4lem  4526  2ralunsn  4896  iuneq2  5015  disjxun  5146  triin  5282  asymref2  6123  cnvpo  6291  dfpo2  6300  fncnv  6626  fnres  6682  mptfnf  6690  fnopabg  6692  mpteqb  7024  eqfnfv3  7042  fvn0ssdmfun  7084  caoftrn  7723  poseq  8163  wfr3g  8328  iiner  8808  ixpeq2  8930  ixpin  8942  ixpfi2  9375  wemaplem2  9571  frr3g  9780  dfac5  10152  kmlem6  10179  eltsk2g  10775  intgru  10838  axgroth6  10852  fsequb  13973  rexanuz  15325  rexanre  15326  cau3lem  15334  rlimcn3  15567  o1of2  15590  o1rlimmul  15596  climbdd  15651  sqrt2irr  16226  gcdcllem1  16474  pc11  16849  prmreclem2  16886  catpropd  17689  issubc3  17835  fucinv  17965  ispos2  18307  issubg3  19099  issubg4  19100  pmtrdifwrdel2  19441  ringsrg  20233  iunocv  21613  cply1mul  22215  scmatf1  22446  cpmatsubgpmat  22635  tgval2  22872  1stcelcls  23378  ptclsg  23532  ptcnplem  23538  fbun  23757  txflf  23923  ucncn  24203  prdsmet  24289  metequiv  24431  metequiv2  24432  ncvsi  25092  iscau4  25220  cmetcaulem  25229  evthicc2  25402  ismbfcn  25571  mbfi1flimlem  25665  rolle  25935  itgsubst  25997  plydivex  26245  ulmcaulem  26343  ulmcau  26344  ulmbdd  26347  ulmcn  26348  mumullem2  27125  2sqlem6  27369  tgcgr4  28348  axpasch  28765  axeuclid  28787  axcontlem2  28789  axcontlem4  28791  axcontlem7  28794  vtxd0nedgb  29315  fusgrregdegfi  29396  rusgr1vtxlem  29414  uspgr2wlkeq  29473  wlkdlem4  29512  lfgriswlk  29515  frgrreg  30217  frgrregord013  30218  friendshipgt3  30221  ocsh  31106  spanuni  31367  riesz4i  31886  leopadd  31955  leoptri  31959  leoptr  31960  inpr0  32341  disjunsn  32397  voliune  33848  volfiniune  33849  eulerpartlemr  33994  eulerpartlemn  34001  nummin  34714  fmlasucdisj  35009  wzel  35420  neibastop1  35843  phpreu  37077  ptrecube  37093  poimirlem23  37116  poimirlem27  37120  ovoliunnfl  37135  voliunnfl  37137  volsupnfl  37138  itg2addnc  37147  inixp  37201  rngoueqz  37413  intidl  37502  pclclN  39364  tendoeq2  40247  deg1gprod  41612  mzpincl  42154  lerabdioph  42225  ltrabdioph  42228  nerabdioph  42229  dvdsrabdioph  42230  dford3lem1  42447  gneispace  43564  ssrabf  44480  r19.28zf  44530  climxrre  45138  stoweidlem7  45395  stoweidlem54  45442  dirkercncflem3  45493  ply1mulgsumlem1  47454  ldepsnlinclem1  47573  ldepsnlinclem2  47574