Theorem r19.26 3172

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 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3162	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3162	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 514	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 472	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3158	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 409	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 211	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∀wral 3140

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 209  df-an 399  df-ral 3145

This theorem is referenced by:  r19.26-2  3173  r19.26-3  3174  ralbiim  3176  r19.27v  3186  r19.27vOLD  3187  r19.28v  3188  reu8  3726  ssrab  4051  r19.28z  4445  r19.27z  4452  ralnralall  4460  2reu4lem  4467  2ralunsn  4827  iuneq2  4940  disjxun  5066  triin  5189  asymref2  5979  cnvpo  6140  fncnv  6429  fnres  6476  mptfnf  6485  fnopabg  6487  mpteqb  6789  eqfnfv3  6806  fvn0ssdmfun  6844  caoftrn  7446  wfr3g  7955  iiner  8371  ixpeq2  8477  ixpin  8489  ixpfi2  8824  wemaplem2  9013  dfac5  9556  kmlem6  9583  eltsk2g  10175  intgru  10238  axgroth6  10252  fsequb  13346  rexanuz  14707  rexanre  14708  cau3lem  14716  rlimcn2  14949  o1of2  14971  o1rlimmul  14977  climbdd  15030  sqrt2irr  15604  gcdcllem1  15850  pc11  16218  prmreclem2  16255  catpropd  16981  issubc3  17121  fucinv  17245  ispos2  17560  issubg3  18299  issubg4  18300  pmtrdifwrdel2  18616  ringsrg  19341  cply1mul  20464  iunocv  20827  scmatf1  21142  cpmatsubgpmat  21330  tgval2  21566  1stcelcls  22071  ptclsg  22225  ptcnplem  22231  fbun  22450  txflf  22616  ucncn  22896  prdsmet  22982  metequiv  23121  metequiv2  23122  ncvsi  23757  iscau4  23884  cmetcaulem  23893  evthicc2  24063  ismbfcn  24232  mbfi1flimlem  24325  rolle  24589  itgsubst  24648  plydivex  24888  ulmcaulem  24984  ulmcau  24985  ulmbdd  24988  ulmcn  24989  mumullem2  25759  2sqlem6  26001  tgcgr4  26319  axpasch  26729  axeuclid  26751  axcontlem2  26753  axcontlem4  26755  axcontlem7  26758  vtxd0nedgb  27272  fusgrregdegfi  27353  rusgr1vtxlem  27371  uspgr2wlkeq  27429  wlkdlem4  27469  lfgriswlk  27472  frgrreg  28175  frgrregord013  28176  friendshipgt3  28179  ocsh  29062  spanuni  29323  riesz4i  29842  leopadd  29911  leoptri  29915  leoptr  29916  inpr0  30294  disjunsn  30346  voliune  31490  volfiniune  31491  eulerpartlemr  31634  eulerpartlemn  31641  fmlasucdisj  32648  dfpo2  32993  poseq  33097  wzel  33113  frr3g  33123  ssltun2  33272  neibastop1  33709  phpreu  34878  ptrecube  34894  poimirlem23  34917  poimirlem27  34921  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  itg2addnc  34948  inixp  35005  rngoueqz  35220  intidl  35309  pclclN  37029  tendoeq2  37912  mzpincl  39338  lerabdioph  39409  ltrabdioph  39412  nerabdioph  39413  dvdsrabdioph  39414  dford3lem1  39630  gneispace  40491  ssrabf  41388  climxrre  42038  stoweidlem7  42299  stoweidlem54  42346  dirkercncflem3  42397  2ralbiim  43310  ply1mulgsumlem1  44447  ldepsnlinclem1  44567  ldepsnlinclem2  44568