Theorem r19.26 3091

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

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

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 3045

This theorem is referenced by:  r19.26-3  3092  ralbiim  3093  2ralbiim  3112  r19.26-2  3118  r19.27v  3164  r19.28v  3166  reu8  3701  ssrab  4032  r19.28z  4457  r19.27z  4464  ralf0  4473  ralnralall  4474  2reu4lem  4481  2ralunsn  4855  iuneq2  4971  disjxun  5100  triin  5226  asymref2  6078  cnvpo  6248  dfpo2  6257  fncnv  6573  fnres  6627  mptfnf  6635  fnopabg  6637  mpteqb  6969  eqfnfv3  6987  fvn0ssdmfun  7028  caoftrn  7674  poseq  8114  wfr3g  8275  iiner  8739  ixpeq2  8861  ixpin  8873  ixpfi2  9277  wemaplem2  9476  frr3g  9685  dfac5  10058  kmlem6  10085  eltsk2g  10680  intgru  10743  axgroth6  10757  fsequb  13916  rexanuz  15288  rexanre  15289  cau3lem  15297  rlimcn3  15532  o1of2  15555  o1rlimmul  15561  climbdd  15614  sqrt2irr  16193  gcdcllem1  16445  pc11  16827  prmreclem2  16864  catpropd  17646  issubc3  17787  fucinv  17914  ispos2  18252  issubg3  19052  issubg4  19053  pmtrdifwrdel2  19392  ringsrg  20182  iunocv  21566  cply1mul  22159  scmatf1  22394  cpmatsubgpmat  22583  tgval2  22819  1stcelcls  23324  ptclsg  23478  ptcnplem  23484  fbun  23703  txflf  23869  ucncn  24148  prdsmet  24234  metequiv  24373  metequiv2  24374  ncvsi  25027  iscau4  25155  cmetcaulem  25164  evthicc2  25337  ismbfcn  25506  mbfi1flimlem  25599  rolle  25870  itgsubst  25932  plydivex  26181  ulmcaulem  26279  ulmcau  26280  ulmbdd  26283  ulmcn  26284  mumullem2  27066  2sqlem6  27310  tgcgr4  28434  axpasch  28844  axeuclid  28866  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  vtxd0nedgb  29392  fusgrregdegfi  29473  rusgr1vtxlem  29491  uspgr2wlkeq  29549  wlkdlem4  29587  lfgriswlk  29590  frgrreg  30296  frgrregord013  30297  friendshipgt3  30300  ocsh  31185  spanuni  31446  riesz4i  31965  leopadd  32034  leoptri  32038  leoptr  32039  inpr0  32434  disjunsn  32496  voliune  34192  volfiniune  34193  eulerpartlemr  34338  eulerpartlemn  34345  nummin  35054  fmlasucdisj  35359  wzel  35785  neibastop1  36320  numiunnum  36431  phpreu  37571  ptrecube  37587  poimirlem23  37610  poimirlem27  37614  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  itg2addnc  37641  inixp  37695  rngoueqz  37907  intidl  37996  pclclN  39858  tendoeq2  40741  deg1gprod  42101  mzpincl  42695  lerabdioph  42766  ltrabdioph  42769  nerabdioph  42770  dvdsrabdioph  42771  dford3lem1  42988  gneispace  44096  ssrabf  45081  r19.28zf  45126  climxrre  45721  stoweidlem7  45978  stoweidlem54  46025  dirkercncflem3  46076  ply1mulgsumlem1  48348  ldepsnlinclem1  48467  ldepsnlinclem2  48468  iinxp  48792  nelsubc2  49031