Theorem r19.26 3112

Description: Restricted quantifier version of 19.26 1874. (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 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3084	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3084	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 513	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 471	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3086	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 408	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  r19.26-3  3113  ralbiim  3114  2ralbiim  3133  r19.26-2  3139  r19.27v  3188  r19.28v  3190  reu8  3730  ssrab  4071  r19.28z  4498  r19.27z  4505  ralf0  4514  ralnralall  4519  2reu4lem  4526  2ralunsn  4896  iuneq2  5017  disjxun  5147  triin  5283  asymref2  6119  cnvpo  6287  dfpo2  6296  fncnv  6622  fnres  6678  mptfnf  6686  fnopabg  6688  mpteqb  7018  eqfnfv3  7035  fvn0ssdmfun  7077  caoftrn  7708  poseq  8144  wfr3g  8307  iiner  8783  ixpeq2  8905  ixpin  8917  ixpfi2  9350  wemaplem2  9542  frr3g  9751  dfac5  10123  kmlem6  10150  eltsk2g  10746  intgru  10809  axgroth6  10823  fsequb  13940  rexanuz  15292  rexanre  15293  cau3lem  15301  rlimcn3  15534  o1of2  15557  o1rlimmul  15563  climbdd  15618  sqrt2irr  16192  gcdcllem1  16440  pc11  16813  prmreclem2  16850  catpropd  17653  issubc3  17799  fucinv  17926  ispos2  18268  issubg3  19024  issubg4  19025  pmtrdifwrdel2  19354  ringsrg  20109  iunocv  21234  cply1mul  21818  scmatf1  22033  cpmatsubgpmat  22222  tgval2  22459  1stcelcls  22965  ptclsg  23119  ptcnplem  23125  fbun  23344  txflf  23510  ucncn  23790  prdsmet  23876  metequiv  24018  metequiv2  24019  ncvsi  24668  iscau4  24796  cmetcaulem  24805  evthicc2  24977  ismbfcn  25146  mbfi1flimlem  25240  rolle  25507  itgsubst  25566  plydivex  25810  ulmcaulem  25906  ulmcau  25907  ulmbdd  25910  ulmcn  25911  mumullem2  26684  2sqlem6  26926  tgcgr4  27782  axpasch  28199  axeuclid  28221  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  vtxd0nedgb  28745  fusgrregdegfi  28826  rusgr1vtxlem  28844  uspgr2wlkeq  28903  wlkdlem4  28942  lfgriswlk  28945  frgrreg  29647  frgrregord013  29648  friendshipgt3  29651  ocsh  30536  spanuni  30797  riesz4i  31316  leopadd  31385  leoptri  31389  leoptr  31390  inpr0  31769  disjunsn  31825  voliune  33227  volfiniune  33228  eulerpartlemr  33373  eulerpartlemn  33380  nummin  34094  fmlasucdisj  34390  wzel  34796  neibastop1  35244  phpreu  36472  ptrecube  36488  poimirlem23  36511  poimirlem27  36515  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnc  36542  inixp  36596  rngoueqz  36808  intidl  36897  pclclN  38762  tendoeq2  39645  mzpincl  41472  lerabdioph  41543  ltrabdioph  41546  nerabdioph  41547  dvdsrabdioph  41548  dford3lem1  41765  gneispace  42885  ssrabf  43803  r19.28zf  43853  climxrre  44466  stoweidlem7  44723  stoweidlem54  44770  dirkercncflem3  44821  ply1mulgsumlem1  47067  ldepsnlinclem1  47186  ldepsnlinclem2  47187