Theorem r19.26 3092

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

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

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

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

This theorem is referenced by:  r19.26-3  3093  ralbiim  3094  2ralbiim  3113  r19.26-2  3119  r19.27v  3167  r19.28v  3169  reu8  3707  ssrab  4039  r19.28z  4464  r19.27z  4471  ralf0  4480  ralnralall  4481  2reu4lem  4488  2ralunsn  4862  iuneq2  4978  disjxun  5108  triin  5234  asymref2  6093  cnvpo  6263  dfpo2  6272  fncnv  6592  fnres  6648  mptfnf  6656  fnopabg  6658  mpteqb  6990  eqfnfv3  7008  fvn0ssdmfun  7049  caoftrn  7697  poseq  8140  wfr3g  8301  iiner  8765  ixpeq2  8887  ixpin  8899  ixpfi2  9308  wemaplem2  9507  frr3g  9716  dfac5  10089  kmlem6  10116  eltsk2g  10711  intgru  10774  axgroth6  10788  fsequb  13947  rexanuz  15319  rexanre  15320  cau3lem  15328  rlimcn3  15563  o1of2  15586  o1rlimmul  15592  climbdd  15645  sqrt2irr  16224  gcdcllem1  16476  pc11  16858  prmreclem2  16895  catpropd  17677  issubc3  17818  fucinv  17945  ispos2  18283  issubg3  19083  issubg4  19084  pmtrdifwrdel2  19423  ringsrg  20213  iunocv  21597  cply1mul  22190  scmatf1  22425  cpmatsubgpmat  22614  tgval2  22850  1stcelcls  23355  ptclsg  23509  ptcnplem  23515  fbun  23734  txflf  23900  ucncn  24179  prdsmet  24265  metequiv  24404  metequiv2  24405  ncvsi  25058  iscau4  25186  cmetcaulem  25195  evthicc2  25368  ismbfcn  25537  mbfi1flimlem  25630  rolle  25901  itgsubst  25963  plydivex  26212  ulmcaulem  26310  ulmcau  26311  ulmbdd  26314  ulmcn  26315  mumullem2  27097  2sqlem6  27341  tgcgr4  28465  axpasch  28875  axeuclid  28897  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  vtxd0nedgb  29423  fusgrregdegfi  29504  rusgr1vtxlem  29522  uspgr2wlkeq  29581  wlkdlem4  29620  lfgriswlk  29623  frgrreg  30330  frgrregord013  30331  friendshipgt3  30334  ocsh  31219  spanuni  31480  riesz4i  31999  leopadd  32068  leoptri  32072  leoptr  32073  inpr0  32468  disjunsn  32530  voliune  34226  volfiniune  34227  eulerpartlemr  34372  eulerpartlemn  34379  nummin  35088  fmlasucdisj  35393  wzel  35819  neibastop1  36354  numiunnum  36465  phpreu  37605  ptrecube  37621  poimirlem23  37644  poimirlem27  37648  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnc  37675  inixp  37729  rngoueqz  37941  intidl  38030  pclclN  39892  tendoeq2  40775  deg1gprod  42135  mzpincl  42729  lerabdioph  42800  ltrabdioph  42803  nerabdioph  42804  dvdsrabdioph  42805  dford3lem1  43022  gneispace  44130  ssrabf  45115  r19.28zf  45160  climxrre  45755  stoweidlem7  46012  stoweidlem54  46059  dirkercncflem3  46110  ply1mulgsumlem1  48379  ldepsnlinclem1  48498  ldepsnlinclem2  48499  iinxp  48823  nelsubc2  49062