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  54  pm2.18  121  ancl  567  ancr  570  anc2r  577  hbim1  2110  hbim1OLD  2215  ralimia  2934  ceqsalgALT  3204  rspct  3275  elabgt  3316  fvmptt  6208  tfi  6945  fnfi  8123  finsschain  8156  ordiso2  8303  ordtypelem7  8312  dfom3  8427  infdiffi  8438  cantnfp1lem3  8460  cantnf  8473  r1ordg  8524  ttukeylem6  9219  fpwwe2lem8  9338  wunfi  9422  dfnn2  10910  trclfvcotr  13598  psgnunilem3  17739  pgpfac1  18302  fiuncmp  21017  filssufilg  21525  ufileu  21533  pjnormssi  28411  bnj1110  30304  waj-ax  31583  bj-sb  31864  bj-equsal1  31999  bj-equsal2  32000  rdgeqoa  32394  wl-mps  32469  refimssco  36932  atbiffatnnb  39728  elsetrecslem  42243
  Copyright terms: Public domain W3C validator