Theorem r19.26 3122

Description: Restricted quantifier version of 19.26 1902. (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 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑)
3		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓)
5	2, 4	jca 521	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))
6		pm3.2 475	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
7	6	ral2imi 3101	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
8	7	imp 412	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))
9	5, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  r19.26-3  3123  ralbiim  3124  2ralbiim  3141  r19.26-2  3147  r19.27v  3191  r19.28v  3193  reu8  3690  ssrab  3995  r19.28z  4457  r19.27z  4465  ralnralall  4468  2reu4lem  4478  2ralunsn  4825  iuneq2  4970  disjxun  5100  triin  5228  asymref2  6113  cnvpo  6293  dfpo2  6302  fncnv  6618  fnres  6671  mptfnf  6679  fnopabg  6681  mpteqb  7018  eqfnfv3  7036  fvn0ssdmfun  7079  caoftrn  7738  poseq  8182  wfr3g  8345  iiner  8818  ixpeq2  8947  ixpin  8959  ixpfi2  9347  wemaplem2  9548  frr3g  9767  dfac5  10214  kmlem6  10241  eltsk2g  10843  intgru  10906  axgroth6  10920  fsequb  14125  rexanuz  15522  rexanre  15523  cau3lem  15531  rlimcn3  15766  o1of2  15789  o1rlimmul  15795  climbdd  15848  sqrt2irr  16426  gcdcllem1  16678  pc11  17067  prmreclem2  17104  catpropd  17892  issubc3  18033  fucinv  18160  ispos2  18498  issubg3  19364  issubg4  19365  pmtrdifwrdel2  19709  dfring3  20527  ringsrg  20537  iunocv  21996  cply1mul  22623  scmatf1  22855  cpmatsubgpmat  23047  tgval2  23283  1stcelcls  23789  ptclsg  23943  ptcnplem  23949  fbun  24168  txflf  24334  ucncn  24612  prdsmet  24698  metequiv  24837  metequiv2  24838  ncvsi  25481  iscau4  25609  cmetcaulem  25618  evthicc2  25790  ismbfcn  25959  mbfi1flimlem  26052  rolle  26319  itgsubst  26378  plydivex  26627  ulmcaulem  26730  ulmcau  26731  ulmbdd  26734  ulmcn  26735  mumullem2  27516  2sqlem6  27759  oldfib  28772  tgcgr4  29003  axpasch  29528  axeuclid  29550  axcontlem2  29552  axcontlem4  29554  axcontlem7  29557  vtxd0nedgb  30078  fusgrregdegfi  30159  rusgr1vtxlem  30177  uspgr2wlkeq  30235  wlkdlem4  30273  lfgriswlk  30280  frgrreg  31004  frgrregord013  31005  friendshipgt3  31008  ocsh  31894  spanuni  32155  riesz4i  32674  leopadd  32743  leoptri  32747  leoptr  32748  inpr0  33179  disjunsn  33239  voliune  34912  volfiniune  34913  eulerpartlemr  35056  eulerpartlemn  35063  nummin  35780  fmlasucdisj  36282  wzel  36710  neibastop1  37271  numiunnum  37382  phpreu  38664  ptrecube  38675  poimirlem23  38698  poimirlem27  38702  ovoliunnfl  38717  voliunnfl  38719  volsupnfl  38720  itg2addnc  38729  inixp  38799  rngoueqz  39011  intidl  39100  pclclN  41085  tendoeq2  41968  deg1gprod  43327  mzpincl  43882  lerabdioph  43949  ltrabdioph  43952  nerabdioph  43953  dvdsrabdioph  43954  dford3lem1  44170  gneispace  45271  ssrabf  46265  r19.28zf  46310  climxrre  46896  stoweidlem7  47153  stoweidlem54  47200  dirkercncflem3  47251  ply1mulgsumlem1  49634  ldepsnlinclem1  49753  ldepsnlinclem2  49754  iinxp  50078  nelsubc2  50319