Theorem r19.26 3093

Description: Restricted quantifier version of 19.26 1838. (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 472	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 2981	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 476	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 2981	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 553	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 462	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 2976	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 444	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 199	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 383  ∀wral 2941

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946

This theorem is referenced by:  r19.26-2  3094  r19.26-3  3095  ralbiim  3098  r19.27v  3099  r19.35  3113  reu8  3435  ssrab  3713  r19.28z  4096  r19.27z  4103  ralnralall  4113  ssdifsn  4351  2ralunsn  4455  iuneq2  4569  disjxun  4683  asymref2  5548  cnvpo  5711  fncnv  6000  fnres  6045  mptfnf  6053  fnopabg  6055  mpteqb  6338  eqfnfv3  6353  fvn0ssdmfun  6390  caoftrn  6974  wfr3g  7458  iiner  7862  ixpeq2  7964  ixpin  7975  ixpfi2  8305  wemaplem2  8493  dfac5  8989  kmlem6  9015  eltsk2g  9611  intgru  9674  axgroth6  9688  fsequb  12814  rexanuz  14129  rexanre  14130  cau3lem  14138  rlimcn2  14365  o1of2  14387  o1rlimmul  14393  climbdd  14446  sqrt2irr  15023  gcdcllem1  15268  pc11  15631  prmreclem2  15668  catpropd  16416  issubc3  16556  fucinv  16680  ispos2  16995  issubg3  17659  issubg4  17660  pmtrdifwrdel2  17952  ringsrg  18635  cply1mul  19712  iunocv  20073  scmatf1  20385  cpmatsubgpmat  20573  tgval2  20808  1stcelcls  21312  ptclsg  21466  ptcnplem  21472  fbun  21691  txflf  21857  ucncn  22136  prdsmet  22222  metequiv  22361  metequiv2  22362  ncvsi  22997  iscau4  23123  cmetcaulem  23132  evthicc2  23275  ismbfcn  23443  mbfi1flimlem  23534  rolle  23798  itgsubst  23857  plydivex  24097  ulmcaulem  24193  ulmcau  24194  ulmbdd  24197  ulmcn  24198  mumullem2  24951  2sqlem6  25193  tgcgr4  25471  axpasch  25866  axeuclid  25888  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  vtxd0nedgb  26440  fusgrregdegfi  26521  rusgr1vtxlem  26539  uspgr2wlkeq  26598  wlkdlem4  26638  lfgriswlk  26641  frgrreg  27381  frgrregord013  27382  friendshipgt3  27385  ocsh  28270  spanuni  28531  riesz4i  29050  leopadd  29119  leoptri  29123  leoptr  29124  disjunsn  29533  voliune  30420  volfiniune  30421  eulerpartlemr  30564  eulerpartlemn  30571  dfpo2  31771  poseq  31878  wzel  31894  frr3g  31904  ssltun2  32041  neibastop1  32479  phpreu  33523  ptrecube  33539  poimirlem23  33562  poimirlem27  33566  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  itg2addnc  33594  inixp  33653  rngoueqz  33869  intidl  33958  pclclN  35495  tendoeq2  36379  mzpincl  37614  lerabdioph  37686  ltrabdioph  37689  nerabdioph  37690  dvdsrabdioph  37691  dford3lem1  37910  gneispace  38749  ssrabf  39612  climxrre  40300  stoweidlem7  40542  stoweidlem54  40589  dirkercncflem3  40640  2ralbiim  41495  2reu4a  41510  ply1mulgsumlem1  42499  ldepsnlinclem1  42619  ldepsnlinclem2  42620