Theorem r19.26 3117

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

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

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

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

This theorem is referenced by:  r19.26-3  3118  ralbiim  3119  2ralbiim  3138  r19.26-2  3144  r19.27v  3194  r19.28v  3196  reu8  3755  ssrab  4096  r19.28z  4521  r19.27z  4528  ralf0  4537  ralnralall  4538  2reu4lem  4545  2ralunsn  4919  iuneq2  5034  disjxun  5164  triin  5300  asymref2  6149  cnvpo  6318  dfpo2  6327  fncnv  6651  fnres  6707  mptfnf  6715  fnopabg  6717  mpteqb  7048  eqfnfv3  7066  fvn0ssdmfun  7108  caoftrn  7753  poseq  8199  wfr3g  8363  iiner  8847  ixpeq2  8969  ixpin  8981  ixpfi2  9420  wemaplem2  9616  frr3g  9825  dfac5  10198  kmlem6  10225  eltsk2g  10820  intgru  10883  axgroth6  10897  fsequb  14026  rexanuz  15394  rexanre  15395  cau3lem  15403  rlimcn3  15636  o1of2  15659  o1rlimmul  15665  climbdd  15720  sqrt2irr  16297  gcdcllem1  16545  pc11  16927  prmreclem2  16964  catpropd  17767  issubc3  17913  fucinv  18043  ispos2  18385  issubg3  19184  issubg4  19185  pmtrdifwrdel2  19528  ringsrg  20320  iunocv  21722  cply1mul  22321  scmatf1  22558  cpmatsubgpmat  22747  tgval2  22984  1stcelcls  23490  ptclsg  23644  ptcnplem  23650  fbun  23869  txflf  24035  ucncn  24315  prdsmet  24401  metequiv  24543  metequiv2  24544  ncvsi  25204  iscau4  25332  cmetcaulem  25341  evthicc2  25514  ismbfcn  25683  mbfi1flimlem  25777  rolle  26048  itgsubst  26110  plydivex  26357  ulmcaulem  26455  ulmcau  26456  ulmbdd  26459  ulmcn  26460  mumullem2  27241  2sqlem6  27485  tgcgr4  28557  axpasch  28974  axeuclid  28996  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  vtxd0nedgb  29524  fusgrregdegfi  29605  rusgr1vtxlem  29623  uspgr2wlkeq  29682  wlkdlem4  29721  lfgriswlk  29724  frgrreg  30426  frgrregord013  30427  friendshipgt3  30430  ocsh  31315  spanuni  31576  riesz4i  32095  leopadd  32164  leoptri  32168  leoptr  32169  inpr0  32560  disjunsn  32616  voliune  34193  volfiniune  34194  eulerpartlemr  34339  eulerpartlemn  34346  nummin  35067  fmlasucdisj  35367  wzel  35788  neibastop1  36325  numiunnum  36436  phpreu  37564  ptrecube  37580  poimirlem23  37603  poimirlem27  37607  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnc  37634  inixp  37688  rngoueqz  37900  intidl  37989  pclclN  39848  tendoeq2  40731  deg1gprod  42097  mzpincl  42690  lerabdioph  42761  ltrabdioph  42764  nerabdioph  42765  dvdsrabdioph  42766  dford3lem1  42983  gneispace  44096  ssrabf  45016  r19.28zf  45064  climxrre  45671  stoweidlem7  45928  stoweidlem54  45975  dirkercncflem3  46026  ply1mulgsumlem1  48115  ldepsnlinclem1  48234  ldepsnlinclem2  48235