Theorem r19.26 3096

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 483	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3088	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3088	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 512	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 470	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 407	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3070

This theorem is referenced by:  r19.26-2  3097  r19.26-3  3098  ralbiim  3100  2ralbiim  3101  r19.27v  3116  r19.28v  3117  reu8  3669  ssrab  4007  r19.28z  4429  r19.27z  4436  ralf0  4445  ralnralall  4450  2reu4lem  4457  2ralunsn  4827  iuneq2  4944  disjxun  5073  triin  5207  asymref2  6027  cnvpo  6194  dfpo2  6203  fncnv  6514  fnres  6568  mptfnf  6577  fnopabg  6579  mpteqb  6903  eqfnfv3  6920  fvn0ssdmfun  6961  caoftrn  7580  wfr3g  8147  iiner  8587  ixpeq2  8708  ixpin  8720  ixpfi2  9126  wemaplem2  9315  frr3g  9523  dfac5  9893  kmlem6  9920  eltsk2g  10516  intgru  10579  axgroth6  10593  fsequb  13704  rexanuz  15066  rexanre  15067  cau3lem  15075  rlimcn3  15308  o1of2  15331  o1rlimmul  15337  climbdd  15392  sqrt2irr  15967  gcdcllem1  16215  pc11  16590  prmreclem2  16627  catpropd  17427  issubc3  17573  fucinv  17700  ispos2  18042  issubg3  18782  issubg4  18783  pmtrdifwrdel2  19103  ringsrg  19837  iunocv  20895  cply1mul  21474  scmatf1  21689  cpmatsubgpmat  21878  tgval2  22115  1stcelcls  22621  ptclsg  22775  ptcnplem  22781  fbun  23000  txflf  23166  ucncn  23446  prdsmet  23532  metequiv  23674  metequiv2  23675  ncvsi  24324  iscau4  24452  cmetcaulem  24461  evthicc2  24633  ismbfcn  24802  mbfi1flimlem  24896  rolle  25163  itgsubst  25222  plydivex  25466  ulmcaulem  25562  ulmcau  25563  ulmbdd  25566  ulmcn  25567  mumullem2  26338  2sqlem6  26580  tgcgr4  26901  axpasch  27318  axeuclid  27340  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  vtxd0nedgb  27864  fusgrregdegfi  27945  rusgr1vtxlem  27963  uspgr2wlkeq  28022  wlkdlem4  28062  lfgriswlk  28065  frgrreg  28767  frgrregord013  28768  friendshipgt3  28771  ocsh  29654  spanuni  29915  riesz4i  30434  leopadd  30503  leoptri  30507  leoptr  30508  inpr0  30889  disjunsn  30942  voliune  32206  volfiniune  32207  eulerpartlemr  32350  eulerpartlemn  32357  nummin  33072  fmlasucdisj  33370  poseq  33811  wzel  33827  neibastop1  34557  phpreu  35770  ptrecube  35786  poimirlem23  35809  poimirlem27  35813  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnc  35840  inixp  35895  rngoueqz  36107  intidl  36196  pclclN  37912  tendoeq2  38795  mzpincl  40563  lerabdioph  40634  ltrabdioph  40637  nerabdioph  40638  dvdsrabdioph  40639  dford3lem1  40855  gneispace  41751  ssrabf  42671  climxrre  43298  stoweidlem7  43555  stoweidlem54  43602  dirkercncflem3  43653  ply1mulgsumlem1  45738  ldepsnlinclem1  45857  ldepsnlinclem2  45858