Theorem a1i 7

Description: Inference derived from axiom ax-1 3. See a1d 14 for an explanation of our informal use of the terms "inference" and "deduction".

Hypothesis

Ref	Expression
a1i.1	|- ph

Assertion

Ref	Expression
a1i	|- (ps -> ph)

Proof of Theorem a1i

Step	Hyp	Ref	Expression
1		a1i.1	. 2 |- ph
2		ax-1 3	. 2 |- (ph -> (ps -> ph))
3	1, 2	ax-mp 6	1 |- (ps -> ph)

Syntax hints:   -> wi 2

This theorem is referenced by:  idd 11  syl 12  a1d 14  syl3 18  syl9 55  pm2.21i 73  pm2.21ni 92  pm4.2i 149  jctl 238  jctr 239  jctil 240  jctir 241  adantl 305  adantlll 313  sylani 356  sylan2i 357  syl5bb 410  syl6bb 414  pm4.71 481  pm4.72 485  mtt 534  2th 540  tbt 541  nbn 542  biantrud 545  biimt 549  bianfd 554  dedlem0a 567  dedlema 569  dedlemb 570  hbth 697  19.33b 771  19.21g 792  cbv3 847  cbval 848  sb4b 862  sbt 899  sbie 904  hbsb4 905  ddelimf2 907  sbidm 912  sbco2 913  a16gb 934  sbcom2 992  bieu 1014  hbeu 1016  bimo 1031  moimv 1044  2euswap 1065  2eu1 1067  2eu3 1069  syl5eq 1136  syl6eq 1140  biral 1223  birex 1224  r19.20si 1254  r19.22si 1275  ralcom2 1314  bireu 1320  ceqsalg 1362  cgsex2g 1368  cgsex4g 1369  sbcgf 1469  zfrep2 1475  zfaus 1480  reuxfr2 1579  ssconb 1598  undif4 1744  elpw2g 1803  elsnc2g 1831  snsspr 1853  prel12 1875  difex2 1951  reuuni4 1959  int0el 1985  eliun 1998  iunab 2023  iun0 2028  iunpw 2040  biopabi 2103  supmo 2156  ordtr2 2257  onint0 2262  oneqmini 2272  bm2.5ii 2274  ord0eln0 2278  trsucss 2309  suceloni 2314  onpwsuc 2315  ordssun 2330  suc11 2341  onuninsuc 2356  limsssuc 2362  unizlim 2364  orduninsuc 2365  onzsl 2367  dfom2 2374  limom 2387  peano3 2392  peano5 2394  brinxp 2466  relss 2480  ssxp 2487  relopab 2494  dmsnsn0 2544  opres 2580  cores 2659  relssdr 2668  funssres 2698  imadif 2714  2elresin 2733  fnopab2 2747  fun 2763  f1ocnvb 2812  tz6.12f 2844  fnsnfv 2861  funfv 2862  fvopab4g 2870  cleqfv 2880  fvelrn 2883  elrnopab 2884  f1fv 2916  f1fveq 2918  cbvfo 2923  isomin 2937  isoini 2938  f1oweOLD 2944  tfrlem4 2952  abianfplem 2999  abianfp 3000  bioprabi 3027  fnoprab2 3039  oprabex2 3045  oprabex3 3046  oprabval2g 3050  oprabval3 3052  1st2val 3097  df1st2 3098  om0r 3142  oaordi 3148  oaord 3149  oaordex 3160  oa00 3161  omordi 3164  nnarcl 3174  nnmordi 3188  nnmord 3189  nnmcan 3190  nnaordex 3191  nnawordex 3192  omsmolem 3195  erth 3219  brecop 3242  eceqopreq 3249  mapss 3270  endom 3289  en2 3305  en3 3306  dom2 3308  fundmen 3333  mapsnen 3334  map1 3335  xpsnen 3339  xpcomen 3343  xpassen 3344  pw2en 3348  sbthbg 3360  canth2 3381  mapdom2lem 3388  mapdom2 3389  mapxpen 3390  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  ssenen 3399  phplem5 3407  nneneq 3408  php3 3411  onfin 3415  pssnn 3428  unblem1 3431  unfilem1 3438  unfi 3441  fiint 3445  inf0 3457  inf3lem3 3466  inf3lem4 3467  dfom3 3477  infensuc 3484  r1lim 3497  r1ord3 3501  ranksn 3532  rankuni 3533  ranklon 3540  scott0 3542  cplem1 3545  karden 3551  aceq3lem 3555  aceq4 3557  aceq5lem4 3561  aceq5lem5 3562  aceq6a 3564  ac6lem 3575  kmlem2 3581  kmlem3 3582  zornlem6 3608  zornlem7 3609  zorn2 3612  fodomb 3615  hta 3619  carden 3638  cardlim 3657  cardsdomel 3658  iscard2 3660  cardiun 3665  alephlim 3670  alephon 3671  alephcard 3673  alephnbtwn2 3675  alephord 3680  alephord3 3683  cardaleph 3690  cardalephex 3691  cardinfima 3696  cfsuc 3709  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem4 3746  axpownd 3747  axregnd 3750  axinfndlem1 3751  axacndlem4 3756  zfcndrep 3760  indpi 3828  ltsopq 3869  ltexpq2 3875  prlem934a 3931  prlem936a 3947  reclem4pr 3953  suplem1pr 3955  ltsosr 3997  sqgt0sr 4009  suppsr2 4017  suppsr3 4018  axrecex 4079  axltadd 4085  axmulgt0 4086  axsup 4088  recdivt 4270  lelttrt 4289  ltletrt 4290  leidt 4293  add20 4329  nn1suc 4435  nnleltp1t 4448  nnsub 4450  sup2 4510  sup3 4511  nn0addclt 4551  nn0mulcl 4553  elznn0 4576  nn0subt 4587  zaddclt 4590  elnn0nn 4593  zmulclt 4596  zltp1let 4597  uzind 4603  uzwo 4605  elq 4629  om2uzlt 4654  om2uzran 4655  seqval 4665  sqrlem6 4736  sqrlem12 4742  sqr11 4761  cjclt 4800  facnnt 4870  clim0 4882  ruclem26 4910  infxpidmlem7 4939  infxpidmlem8 4940  infmap2lem2 4952  alephsuc3 4955  hial0 5058  hial2eqt 5060  bcseq 5073  hlim0 5140  hlimreu 5145  occllem6 5185  occllem7 5186  projlem25 5217  projlem26 5218  projlem31 5223  pjthlem7 5231  pjmvalt 5245  osumlem3 5532  osum 5538  stge1 5679  stle0 5680  stadd 5687  stadd3 5689  mdbr3 5729  mdbr4 5730  ssmd1 5734  ssmd2 5735  elat2 5739  atsseq 5745  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem6 5781  mdsymlem7 5782  mdsymlem8 5783

This theorem was proved from axioms:  ax-1 3  ax-mp 6

metamath.org