Theorem r19.26 3111

Description: Restricted quantifier version of 19.26 1873. (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 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 512	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 470	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3085	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 407	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

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

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

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

This theorem is referenced by:  r19.26-3  3112  ralbiim  3113  2ralbiim  3132  r19.26-2  3138  r19.27v  3187  r19.28v  3189  reu8  3728  ssrab  4069  r19.28z  4496  r19.27z  4503  ralf0  4512  ralnralall  4517  2reu4lem  4524  2ralunsn  4894  iuneq2  5015  disjxun  5145  triin  5281  asymref2  6115  cnvpo  6283  dfpo2  6292  fncnv  6618  fnres  6674  mptfnf  6682  fnopabg  6684  mpteqb  7014  eqfnfv3  7031  fvn0ssdmfun  7073  caoftrn  7704  poseq  8140  wfr3g  8303  iiner  8779  ixpeq2  8901  ixpin  8913  ixpfi2  9346  wemaplem2  9538  frr3g  9747  dfac5  10119  kmlem6  10146  eltsk2g  10742  intgru  10805  axgroth6  10819  fsequb  13936  rexanuz  15288  rexanre  15289  cau3lem  15297  rlimcn3  15530  o1of2  15553  o1rlimmul  15559  climbdd  15614  sqrt2irr  16188  gcdcllem1  16436  pc11  16809  prmreclem2  16846  catpropd  17649  issubc3  17795  fucinv  17922  ispos2  18264  issubg3  19018  issubg4  19019  pmtrdifwrdel2  19348  ringsrg  20102  iunocv  21225  cply1mul  21809  scmatf1  22024  cpmatsubgpmat  22213  tgval2  22450  1stcelcls  22956  ptclsg  23110  ptcnplem  23116  fbun  23335  txflf  23501  ucncn  23781  prdsmet  23867  metequiv  24009  metequiv2  24010  ncvsi  24659  iscau4  24787  cmetcaulem  24796  evthicc2  24968  ismbfcn  25137  mbfi1flimlem  25231  rolle  25498  itgsubst  25557  plydivex  25801  ulmcaulem  25897  ulmcau  25898  ulmbdd  25901  ulmcn  25902  mumullem2  26673  2sqlem6  26915  tgcgr4  27771  axpasch  28188  axeuclid  28210  axcontlem2  28212  axcontlem4  28214  axcontlem7  28217  vtxd0nedgb  28734  fusgrregdegfi  28815  rusgr1vtxlem  28833  uspgr2wlkeq  28892  wlkdlem4  28931  lfgriswlk  28934  frgrreg  29636  frgrregord013  29637  friendshipgt3  29640  ocsh  30523  spanuni  30784  riesz4i  31303  leopadd  31372  leoptri  31376  leoptr  31377  inpr0  31756  disjunsn  31812  voliune  33215  volfiniune  33216  eulerpartlemr  33361  eulerpartlemn  33368  nummin  34082  fmlasucdisj  34378  wzel  34784  neibastop1  35232  phpreu  36460  ptrecube  36476  poimirlem23  36499  poimirlem27  36503  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  itg2addnc  36530  inixp  36584  rngoueqz  36796  intidl  36885  pclclN  38750  tendoeq2  39633  mzpincl  41457  lerabdioph  41528  ltrabdioph  41531  nerabdioph  41532  dvdsrabdioph  41533  dford3lem1  41750  gneispace  42870  ssrabf  43788  r19.28zf  43838  climxrre  44452  stoweidlem7  44709  stoweidlem54  44756  dirkercncflem3  44807  ply1mulgsumlem1  47020  ldepsnlinclem1  47139  ldepsnlinclem2  47140