MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a2i Structured version   Visualization version   GIF version

Theorem a2i 14
Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 15. (Contributed by NM, 29-Dec-1992.)
Hypothesis
Ref Expression
a2i.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
a2i ((𝜑𝜓) → (𝜑𝜒))

Proof of Theorem a2i
StepHypRef Expression
1 a2i.1 . 2 (𝜑 → (𝜓𝜒))
2 ax-2 7 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜓) → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-2 7
This theorem is referenced by:  mpd  15  imim2i  16  sylcom  30  pm2.43  56  pm2.18  122  ancl  568  ancr  571  anc2r  578  hbim1  2163  hbim1OLD  2263  ralimia  2979  ceqsalgALT  3262  rspct  3333  elabgt  3379  fvmptt  6339  tfi  7095  fnfi  8279  finsschain  8314  ordiso2  8461  ordtypelem7  8470  dfom3  8582  infdiffi  8593  cantnfp1lem3  8615  cantnf  8628  r1ordg  8679  ttukeylem6  9374  fpwwe2lem8  9497  wunfi  9581  dfnn2  11071  trclfvcotr  13794  psgnunilem3  17962  pgpfac1  18525  fiuncmp  21255  filssufilg  21762  ufileu  21770  pjnormssi  29155  bnj1110  31176  waj-ax  32538  bj-sb  32802  bj-equsal1  32936  bj-equsal2  32937  rdgeqoa  33348  wl-mps  33420  refimssco  38230  atbiffatnnb  41400  elsetrecslem  42770
  Copyright terms: Public domain W3C validator