Theorem r19.26 3122

Description: Restricted quantifier version of 19.26 1890. (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 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 519	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 473	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3101	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 410	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 211	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399  ∀wral 3076

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3077

This theorem is referenced by:  r19.26-3  3123  ralbiim  3124  2ralbiim  3141  r19.26-2  3147  r19.27v  3191  r19.28v  3193  reu8  3696  ssrab  4024  r19.28z  4456  r19.27z  4464  ralnralall  4467  2reu4lem  4477  2ralunsn  4853  iuneq2  4969  disjxun  5098  triin  5224  asymref2  6104  cnvpo  6274  dfpo2  6283  fncnv  6594  fnres  6648  mptfnf  6656  fnopabg  6658  mpteqb  6995  eqfnfv3  7013  fvn0ssdmfun  7055  caoftrn  7701  poseq  8138  wfr3g  8300  iiner  8771  ixpeq2  8893  ixpin  8905  ixpfi2  9293  wemaplem2  9495  frr3g  9714  dfac5  10085  kmlem6  10112  eltsk2g  10709  intgru  10772  axgroth6  10786  fsequb  13988  rexanuz  15373  rexanre  15374  cau3lem  15382  rlimcn3  15617  o1of2  15640  o1rlimmul  15646  climbdd  15699  sqrt2irr  16281  gcdcllem1  16533  pc11  16916  prmreclem2  16953  catpropd  17741  issubc3  17882  fucinv  18009  ispos2  18347  issubg3  19186  issubg4  19187  pmtrdifwrdel2  19526  ringsrg  20347  iunocv  21733  cply1mul  22359  scmatf1  22591  cpmatsubgpmat  22780  tgval2  23016  1stcelcls  23521  ptclsg  23675  ptcnplem  23681  fbun  23900  txflf  24066  ucncn  24344  prdsmet  24430  metequiv  24569  metequiv2  24570  ncvsi  25213  iscau4  25341  cmetcaulem  25350  evthicc2  25522  ismbfcn  25691  mbfi1flimlem  25784  rolle  26052  itgsubst  26111  plydivex  26361  ulmcaulem  26457  ulmcau  26458  ulmbdd  26461  ulmcn  26462  mumullem2  27244  2sqlem6  27487  oldfib  28470  tgcgr4  28700  axpasch  29142  axeuclid  29164  axcontlem2  29166  axcontlem4  29168  axcontlem7  29171  vtxd0nedgb  29689  fusgrregdegfi  29770  rusgr1vtxlem  29788  uspgr2wlkeq  29846  wlkdlem4  29884  lfgriswlk  29887  frgrreg  30596  frgrregord013  30597  friendshipgt3  30600  ocsh  31486  spanuni  31747  riesz4i  32266  leopadd  32335  leoptri  32339  leoptr  32340  inpr0  32731  disjunsn  32794  voliune  34526  volfiniune  34527  eulerpartlemr  34671  eulerpartlemn  34678  nummin  35389  fmlasucdisj  35749  wzel  36172  neibastop1  36719  numiunnum  36830  phpreu  38103  ptrecube  38119  poimirlem23  38142  poimirlem27  38146  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  itg2addnc  38173  inixp  38227  rngoueqz  38439  intidl  38528  pclclN  40515  tendoeq2  41398  deg1gprod  42757  mzpincl  43315  lerabdioph  43382  ltrabdioph  43385  nerabdioph  43386  dvdsrabdioph  43387  dford3lem1  43603  gneispace  44710  ssrabf  45692  r19.28zf  45737  climxrre  46324  stoweidlem7  46581  stoweidlem54  46628  dirkercncflem3  46679  ply1mulgsumlem1  49008  ldepsnlinclem1  49127  ldepsnlinclem2  49128  iinxp  49452  nelsubc2  49690