Theorem r19.26 3094

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

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

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

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

This theorem is referenced by:  r19.26-2  3095  r19.26-3  3096  ralbiim  3098  2ralbiim  3099  r19.27v  3109  r19.28v  3110  reu8  3663  ssrab  4002  r19.28z  4425  r19.27z  4432  ralf0  4441  ralnralall  4446  2reu4lem  4453  2ralunsn  4823  iuneq2  4940  disjxun  5068  triin  5202  asymref2  6011  cnvpo  6179  dfpo2  6188  fncnv  6491  fnres  6543  mptfnf  6552  fnopabg  6554  mpteqb  6876  eqfnfv3  6893  fvn0ssdmfun  6934  caoftrn  7549  wfr3g  8109  iiner  8536  ixpeq2  8657  ixpin  8669  ixpfi2  9047  wemaplem2  9236  frr3g  9445  dfac5  9815  kmlem6  9842  eltsk2g  10438  intgru  10501  axgroth6  10515  fsequb  13623  rexanuz  14985  rexanre  14986  cau3lem  14994  rlimcn3  15227  o1of2  15250  o1rlimmul  15256  climbdd  15311  sqrt2irr  15886  gcdcllem1  16134  pc11  16509  prmreclem2  16546  catpropd  17335  issubc3  17480  fucinv  17607  ispos2  17948  issubg3  18688  issubg4  18689  pmtrdifwrdel2  19009  ringsrg  19743  iunocv  20798  cply1mul  21375  scmatf1  21588  cpmatsubgpmat  21777  tgval2  22014  1stcelcls  22520  ptclsg  22674  ptcnplem  22680  fbun  22899  txflf  23065  ucncn  23345  prdsmet  23431  metequiv  23571  metequiv2  23572  ncvsi  24220  iscau4  24348  cmetcaulem  24357  evthicc2  24529  ismbfcn  24698  mbfi1flimlem  24792  rolle  25059  itgsubst  25118  plydivex  25362  ulmcaulem  25458  ulmcau  25459  ulmbdd  25462  ulmcn  25463  mumullem2  26234  2sqlem6  26476  tgcgr4  26796  axpasch  27212  axeuclid  27234  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  vtxd0nedgb  27758  fusgrregdegfi  27839  rusgr1vtxlem  27857  uspgr2wlkeq  27915  wlkdlem4  27955  lfgriswlk  27958  frgrreg  28659  frgrregord013  28660  friendshipgt3  28663  ocsh  29546  spanuni  29807  riesz4i  30326  leopadd  30395  leoptri  30399  leoptr  30400  inpr0  30781  disjunsn  30834  voliune  32097  volfiniune  32098  eulerpartlemr  32241  eulerpartlemn  32248  nummin  32963  fmlasucdisj  33261  poseq  33729  wzel  33745  neibastop1  34475  phpreu  35688  ptrecube  35704  poimirlem23  35727  poimirlem27  35731  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  itg2addnc  35758  inixp  35813  rngoueqz  36025  intidl  36114  pclclN  37832  tendoeq2  38715  mzpincl  40472  lerabdioph  40543  ltrabdioph  40546  nerabdioph  40547  dvdsrabdioph  40548  dford3lem1  40764  gneispace  41633  ssrabf  42553  climxrre  43181  stoweidlem7  43438  stoweidlem54  43485  dirkercncflem3  43536  ply1mulgsumlem1  45615  ldepsnlinclem1  45734  ldepsnlinclem2  45735