Theorem ralimi 2605

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralimi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 2603	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2203  ∀wral 2520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117  df-ral 2525

This theorem is referenced by:  2ralimi  2606  ral2imi  2607  r19.26  2669  r19.29  2680  rr19.3v  2956  rr19.28v  2957  reu3  3007  uniiunlem  3328  reupick2  3507  uniss2  3945  ss2iun  4006  iineq2  4008  iunss2  4036  disjss2  4088  disjeq2  4089  disjnim  4099  repizf  4226  abnexg  4567  reusv3i  4580  tfis  4705  ssrel2  4840  issref  5145  dmmptg  5260  funco  5392  fununi  5424  fun11uni  5426  funimaexglem  5439  fnmpt  5485  fun11iun  5635  mpteqb  5768  chfnrn  5789  dffo5  5826  ffvresb  5840  fmptcof  5844  dfmptg  5857  mpo2eqb  6163  ralrnmpo  6168  rexrnmpo  6169  uchoice  6331  fnmpo  6398  mpoexxg  6406  smores  6523  riinerm  6842  ixpm  6965  difinfinf  7392  nninfwlpoimlemginf  7467  exmidontriimlem1  7528  onntri13  7548  onntri24  7552  cc4f  7583  cc4n  7585  cauappcvgprlemdisj  7966  caucvgsrlemasr  8105  caucvgsr  8117  suplocsr  8124  rexuz3  11675  recvguniq  11680  cau3lem  11799  caubnd2  11802  rexanre  11905  climi2  11973  climi0  11974  climcaucn  12036  ndvdssub  12616  gcdsupex  12653  gcdsupcl  12654  bezoutlemmo  12702  ptex  13477  mgmidmo  13585  issubg2m  13906  eltg2b  14919  neipsm  15019  lmcvg  15082  txlm  15144  metrest  15371  mulcncflem  15472  wlkvtxeledgg  16339  upgrwlkcompim  16357  upgrwlkvtxedg  16359  upgr2wlkdc  16372  bj-charfunbi  16581  bj-indint  16701  bj-indind  16702  bj-bdfindis  16717  setindis  16737  bdsetindis  16739  pw1dceq  16778  exmidcon  16780  exmidpeirce  16781  neap0mkv  16855