Theorem r19.26 3094

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

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

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 3050

This theorem is referenced by:  r19.26-3  3095  ralbiim  3096  2ralbiim  3113  r19.26-2  3119  r19.27v  3163  r19.28v  3165  reu8  3689  ssrab  4021  r19.28z  4453  r19.27z  4461  ralnralall  4464  2reu4lem  4474  2ralunsn  4849  iuneq2  4964  disjxun  5094  triin  5219  asymref2  6072  cnvpo  6243  dfpo2  6252  fncnv  6563  fnres  6617  mptfnf  6625  fnopabg  6627  mpteqb  6958  eqfnfv3  6976  fvn0ssdmfun  7017  caoftrn  7661  poseq  8098  wfr3g  8259  iiner  8724  ixpeq2  8847  ixpin  8859  ixpfi2  9248  wemaplem2  9450  frr3g  9666  dfac5  10037  kmlem6  10064  eltsk2g  10660  intgru  10723  axgroth6  10737  fsequb  13896  rexanuz  15267  rexanre  15268  cau3lem  15276  rlimcn3  15511  o1of2  15534  o1rlimmul  15540  climbdd  15593  sqrt2irr  16172  gcdcllem1  16424  pc11  16806  prmreclem2  16843  catpropd  17630  issubc3  17771  fucinv  17898  ispos2  18236  issubg3  19072  issubg4  19073  pmtrdifwrdel2  19413  ringsrg  20230  iunocv  21634  cply1mul  22238  scmatf1  22473  cpmatsubgpmat  22662  tgval2  22898  1stcelcls  23403  ptclsg  23557  ptcnplem  23563  fbun  23782  txflf  23948  ucncn  24226  prdsmet  24312  metequiv  24451  metequiv2  24452  ncvsi  25105  iscau4  25233  cmetcaulem  25242  evthicc2  25415  ismbfcn  25584  mbfi1flimlem  25677  rolle  25948  itgsubst  26010  plydivex  26259  ulmcaulem  26357  ulmcau  26358  ulmbdd  26361  ulmcn  26362  mumullem2  27144  2sqlem6  27388  oldfib  28335  tgcgr4  28552  axpasch  28963  axeuclid  28985  axcontlem2  28987  axcontlem4  28989  axcontlem7  28992  vtxd0nedgb  29511  fusgrregdegfi  29592  rusgr1vtxlem  29610  uspgr2wlkeq  29668  wlkdlem4  29706  lfgriswlk  29709  frgrreg  30418  frgrregord013  30419  friendshipgt3  30422  ocsh  31307  spanuni  31568  riesz4i  32087  leopadd  32156  leoptri  32160  leoptr  32161  inpr0  32556  disjunsn  32618  voliune  34335  volfiniune  34336  eulerpartlemr  34480  eulerpartlemn  34487  nummin  35198  fmlasucdisj  35542  wzel  35965  neibastop1  36502  numiunnum  36613  phpreu  37744  ptrecube  37760  poimirlem23  37783  poimirlem27  37787  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  itg2addnc  37814  inixp  37868  rngoueqz  38080  intidl  38169  pclclN  40090  tendoeq2  40973  deg1gprod  42333  mzpincl  42918  lerabdioph  42989  ltrabdioph  42992  nerabdioph  42993  dvdsrabdioph  42994  dford3lem1  43210  gneispace  44317  ssrabf  45300  r19.28zf  45345  climxrre  45936  stoweidlem7  46193  stoweidlem54  46240  dirkercncflem3  46291  ply1mulgsumlem1  48574  ldepsnlinclem1  48693  ldepsnlinclem2  48694  iinxp  49018  nelsubc2  49256