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  3166  r19.28v  3168  reu8  3704  ssrab  4036  r19.28z  4461  r19.27z  4468  ralf0  4477  ralnralall  4478  2reu4lem  4485  2ralunsn  4859  iuneq2  4975  disjxun  5105  triin  5231  asymref2  6090  cnvpo  6260  dfpo2  6269  fncnv  6589  fnres  6645  mptfnf  6653  fnopabg  6655  mpteqb  6987  eqfnfv3  7005  fvn0ssdmfun  7046  caoftrn  7694  poseq  8137  wfr3g  8298  iiner  8762  ixpeq2  8884  ixpin  8896  ixpfi2  9301  wemaplem2  9500  frr3g  9709  dfac5  10082  kmlem6  10109  eltsk2g  10704  intgru  10767  axgroth6  10781  fsequb  13940  rexanuz  15312  rexanre  15313  cau3lem  15321  rlimcn3  15556  o1of2  15579  o1rlimmul  15585  climbdd  15638  sqrt2irr  16217  gcdcllem1  16469  pc11  16851  prmreclem2  16888  catpropd  17670  issubc3  17811  fucinv  17938  ispos2  18276  issubg3  19076  issubg4  19077  pmtrdifwrdel2  19416  ringsrg  20206  iunocv  21590  cply1mul  22183  scmatf1  22418  cpmatsubgpmat  22607  tgval2  22843  1stcelcls  23348  ptclsg  23502  ptcnplem  23508  fbun  23727  txflf  23893  ucncn  24172  prdsmet  24258  metequiv  24397  metequiv2  24398  ncvsi  25051  iscau4  25179  cmetcaulem  25188  evthicc2  25361  ismbfcn  25530  mbfi1flimlem  25623  rolle  25894  itgsubst  25956  plydivex  26205  ulmcaulem  26303  ulmcau  26304  ulmbdd  26307  ulmcn  26308  mumullem2  27090  2sqlem6  27334  tgcgr4  28458  axpasch  28868  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  vtxd0nedgb  29416  fusgrregdegfi  29497  rusgr1vtxlem  29515  uspgr2wlkeq  29574  wlkdlem4  29613  lfgriswlk  29616  frgrreg  30323  frgrregord013  30324  friendshipgt3  30327  ocsh  31212  spanuni  31473  riesz4i  31992  leopadd  32061  leoptri  32065  leoptr  32066  inpr0  32461  disjunsn  32523  voliune  34219  volfiniune  34220  eulerpartlemr  34365  eulerpartlemn  34372  nummin  35081  fmlasucdisj  35386  wzel  35812  neibastop1  36347  numiunnum  36458  phpreu  37598  ptrecube  37614  poimirlem23  37637  poimirlem27  37641  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnc  37668  inixp  37722  rngoueqz  37934  intidl  38023  pclclN  39885  tendoeq2  40768  deg1gprod  42128  mzpincl  42722  lerabdioph  42793  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  dford3lem1  43015  gneispace  44123  ssrabf  45108  r19.28zf  45153  climxrre  45748  stoweidlem7  46005  stoweidlem54  46052  dirkercncflem3  46103  ply1mulgsumlem1  48375  ldepsnlinclem1  48494  ldepsnlinclem2  48495  iinxp  48819  nelsubc2  49058