Theorem r19.26 3096

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

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

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 3052

This theorem is referenced by:  r19.26-3  3097  ralbiim  3098  2ralbiim  3115  r19.26-2  3121  r19.27v  3165  r19.28v  3167  reu8  3691  ssrab  4023  r19.28z  4455  r19.27z  4463  ralnralall  4466  2reu4lem  4476  2ralunsn  4851  iuneq2  4966  disjxun  5096  triin  5221  asymref2  6074  cnvpo  6245  dfpo2  6254  fncnv  6565  fnres  6619  mptfnf  6627  fnopabg  6629  mpteqb  6960  eqfnfv3  6978  fvn0ssdmfun  7019  caoftrn  7663  poseq  8100  wfr3g  8261  iiner  8726  ixpeq2  8849  ixpin  8861  ixpfi2  9250  wemaplem2  9452  frr3g  9668  dfac5  10039  kmlem6  10066  eltsk2g  10662  intgru  10725  axgroth6  10739  fsequb  13898  rexanuz  15269  rexanre  15270  cau3lem  15278  rlimcn3  15513  o1of2  15536  o1rlimmul  15542  climbdd  15595  sqrt2irr  16174  gcdcllem1  16426  pc11  16808  prmreclem2  16845  catpropd  17632  issubc3  17773  fucinv  17900  ispos2  18238  issubg3  19074  issubg4  19075  pmtrdifwrdel2  19415  ringsrg  20232  iunocv  21636  cply1mul  22240  scmatf1  22475  cpmatsubgpmat  22664  tgval2  22900  1stcelcls  23405  ptclsg  23559  ptcnplem  23565  fbun  23784  txflf  23950  ucncn  24228  prdsmet  24314  metequiv  24453  metequiv2  24454  ncvsi  25107  iscau4  25235  cmetcaulem  25244  evthicc2  25417  ismbfcn  25586  mbfi1flimlem  25679  rolle  25950  itgsubst  26012  plydivex  26261  ulmcaulem  26359  ulmcau  26360  ulmbdd  26363  ulmcn  26364  mumullem2  27146  2sqlem6  27390  oldfib  28373  tgcgr4  28603  axpasch  29014  axeuclid  29036  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  vtxd0nedgb  29562  fusgrregdegfi  29643  rusgr1vtxlem  29661  uspgr2wlkeq  29719  wlkdlem4  29757  lfgriswlk  29760  frgrreg  30469  frgrregord013  30470  friendshipgt3  30473  ocsh  31358  spanuni  31619  riesz4i  32138  leopadd  32207  leoptri  32211  leoptr  32212  inpr0  32607  disjunsn  32669  voliune  34386  volfiniune  34387  eulerpartlemr  34531  eulerpartlemn  34538  nummin  35249  fmlasucdisj  35593  wzel  36016  neibastop1  36553  numiunnum  36664  phpreu  37805  ptrecube  37821  poimirlem23  37844  poimirlem27  37848  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  itg2addnc  37875  inixp  37929  rngoueqz  38141  intidl  38230  pclclN  40151  tendoeq2  41034  deg1gprod  42394  mzpincl  42976  lerabdioph  43047  ltrabdioph  43050  nerabdioph  43051  dvdsrabdioph  43052  dford3lem1  43268  gneispace  44375  ssrabf  45358  r19.28zf  45403  climxrre  45994  stoweidlem7  46251  stoweidlem54  46298  dirkercncflem3  46349  ply1mulgsumlem1  48632  ldepsnlinclem1  48751  ldepsnlinclem2  48752  iinxp  49076  nelsubc2  49314