Theorem pm2.43i 64

Description: Inference absorbing redundant antecedent.

Hypothesis

Ref	Expression
pm2.43i.1	⊢ (φ → (φ → ψ))

Assertion

Ref	Expression
pm2.43i	⊢ (φ → ψ)

Proof of Theorem pm2.43i

Step	Hyp	Ref	Expression
1		pm2.43i.1	. 2 ⊢ (φ → (φ → ψ))
2		pm2.43 63	. 2 ⊢ ((φ → (φ → ψ)) → (φ → ψ))
3	1, 2	ax-mp 7	1 ⊢ (φ → ψ)

Syntax hints:   → wi 3

This theorem is referenced by:  pm2.18 81  anidm 432  anidms 434  anabsi5 495  ibi 591  3anidm12 880  ax4 970  equid 1124  ax10 1139  hbae 1143  hbequid 1167  equid1 1267  ax11inda 1369  vtoclgaf 1847  sbcth2 1978  ssiun2s 2589  copsexg 2787  reuuni2f 2878  tz7.7 2968  nsuceq0 3048  tfrlem9 3910  tfrlem11 3912  oprabvalig 4015  omcl 4161  oecl 4162  odi 4200  nnmcl 4220  nnecl 4221  sbth 4443  zorn2lem6 4773  zorn2lem7 4774  mulcanpi 5007  indpi 5014  prcdpq 5077  ltaddpr 5120  reclem2pr 5137  reclem3pr 5138  lemulge11t 5812  lediv2it 5853  nn1suc 5895  ser1add2 6283  ser1add 6284  2climnn 7047  2climnn0 7048  infcvgaux2 7163  alephexp2 7536  strlem1 10115  gelsupvalOLD 10354  ompfl2OLD 10363  uninqs 10378  infi1 10383  fiiu 10386  ficli 10404  fiiu2 10413  bsi 10418  hmphre 10453  hmeogrp 10461  homcard 10462  fillsb 10471  filint 10473  fipfil2 10475  filintf 10479  filint2 10482  iintlem1 10512

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain