Theorem r19.26 3250

Description: Restricted quantifier version of 19.26 1916. (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 476	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3134	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 479	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3134	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 507	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 463	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3129	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 397	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 201	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 386  ∀wral 3090

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ral 3095

This theorem is referenced by:  r19.26-2  3251  r19.26-3  3252  ralbiim  3255  r19.27v  3256  r19.35  3270  reu8  3614  ssrab  3901  r19.28z  4286  r19.27z  4293  ralnralall  4301  2ralunsn  4660  iuneq2  4772  disjxun  4886  triin  5004  asymref2  5770  cnvpo  5929  fncnv  6209  fnres  6255  mptfnf  6263  fnopabg  6265  mpteqb  6562  eqfnfv3  6578  fvn0ssdmfun  6616  caoftrn  7211  wfr3g  7697  iiner  8104  ixpeq2  8210  ixpin  8221  ixpfi2  8554  wemaplem2  8743  dfac5  9286  kmlem6  9314  eltsk2g  9910  intgru  9973  axgroth6  9987  fsequb  13097  rexanuz  14496  rexanre  14497  cau3lem  14505  rlimcn2  14733  o1of2  14755  o1rlimmul  14761  climbdd  14814  sqrt2irr  15386  gcdcllem1  15631  pc11  15992  prmreclem2  16029  catpropd  16758  issubc3  16898  fucinv  17022  ispos2  17338  issubg3  18000  issubg4  18001  pmtrdifwrdel2  18293  ringsrg  18980  cply1mul  20064  iunocv  20428  scmatf1  20746  cpmatsubgpmat  20936  tgval2  21172  1stcelcls  21677  ptclsg  21831  ptcnplem  21837  fbun  22056  txflf  22222  ucncn  22501  prdsmet  22587  metequiv  22726  metequiv2  22727  ncvsi  23362  iscau4  23489  cmetcaulem  23498  evthicc2  23668  ismbfcn  23837  mbfi1flimlem  23930  rolle  24194  itgsubst  24253  plydivex  24493  ulmcaulem  24589  ulmcau  24590  ulmbdd  24593  ulmcn  24594  mumullem2  25362  2sqlem6  25604  tgcgr4  25886  axpasch  26294  axeuclid  26316  axcontlem2  26318  axcontlem4  26320  axcontlem7  26323  vtxd0nedgb  26840  fusgrregdegfi  26921  rusgr1vtxlem  26939  uspgr2wlkeq  26997  wlkdlem4  27040  lfgriswlk  27043  frgrreg  27830  frgrregord013  27831  friendshipgt3  27834  ocsh  28718  spanuni  28979  riesz4i  29498  leopadd  29567  leoptri  29571  leoptr  29572  disjunsn  29974  voliune  30894  volfiniune  30895  eulerpartlemr  31038  eulerpartlemn  31045  dfpo2  32243  poseq  32346  wzel  32362  frr3g  32372  ssltun2  32509  neibastop1  32946  phpreu  34023  ptrecube  34040  poimirlem23  34063  poimirlem27  34067  ovoliunnfl  34082  voliunnfl  34084  volsupnfl  34085  itg2addnc  34094  inixp  34153  rngoueqz  34368  intidl  34457  pclclN  36050  tendoeq2  36933  mzpincl  38267  lerabdioph  38339  ltrabdioph  38342  nerabdioph  38343  dvdsrabdioph  38344  dford3lem1  38562  gneispace  39398  ssrabf  40237  climxrre  40900  stoweidlem7  41161  stoweidlem54  41208  dirkercncflem3  41259  2ralbiim  42143  2reu4a  42160  ply1mulgsumlem1  43199  ldepsnlinclem1  43319  ldepsnlinclem2  43320