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  2109  hbim1OLD  2214  ralimia  2933  ceqsalgALT  3203  rspct  3274  elabgt  3315  fvmptt  6193  tfi  6922  fnfi  8100  finsschain  8133  ordiso2  8280  ordtypelem7  8289  dfom3  8404  infdiffi  8415  cantnfp1lem3  8437  cantnf  8450  r1ordg  8501  ttukeylem6  9196  fpwwe2lem8  9315  wunfi  9399  dfnn2  10880  trclfvcotr  13544  psgnunilem3  17685  pgpfac1  18248  fiuncmp  20959  filssufilg  21467  ufileu  21475  pjnormssi  28217  bnj1110  30110  waj-ax  31389  bj-sb  31670  bj-equsal1  31805  bj-equsal2  31806  rdgeqoa  32190  wl-mps  32265  refimssco  36728  atbiffatnnb  39525
  Copyright terms: Public domain W3C validator