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  53  pm2.18  120  ancl  566  ancr  569  anc2r  576  hbim1  2049  ralimia  2838  ceqsalgALT  3108  rspct  3179  elabgt  3220  fvmptt  6091  tfi  6820  fnfi  7998  finsschain  8031  ordiso2  8178  ordtypelem7  8187  dfom3  8302  infdiffi  8313  cantnfp1lem3  8335  cantnf  8348  r1ordg  8399  ttukeylem6  9094  fpwwe2lem8  9213  wunfi  9297  dfnn2  10787  trclfvcotr  13455  psgnunilem3  17629  pgpfac1  18207  fiuncmp  20918  filssufilg  21426  ufileu  21434  pjnormssi  28200  bnj1110  30150  waj-ax  31418  bj-sb  31699  bj-equsal1  31841  bj-equsal2  31842  rdgeqoa  32226  wl-mps  32343  refimssco  36814  atbiffatnnb  39622
  Copyright terms: Public domain W3C validator