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.18OLD  129  ancl  547  ancr  549  anc2r  557  hbim1  2305  ralimia  3145  ceqsalgALT  3509  rspct  3588  elabgt  3641  fvmptt  6764  tfi  7546  fnfi  8774  finsschain  8809  ordiso2  8957  ordtypelem7  8966  dfom3  9088  infdiffi  9099  cantnfp1lem3  9121  cantnf  9134  r1ordg  9185  ttukeylem6  9914  fpwwe2lem8  10037  wunfi  10121  dfnn2  11629  trclfvcotr  14349  psgnunilem3  18603  pgpfac1  19181  fiuncmp  21988  filssufilg  22495  ufileu  22503  pjnormssi  29930  bnj1110  32262  waj-ax  33770  bj-nnclav  33892  bj-peircestab  33896  bj-sb  34029  bj-equsal1  34155  bj-equsal2  34156  rdgeqoa  34668  wl-mps  34788  refimssco  40102  atbiffatnnb  43296  rexrsb  43446  elsetrecslem  44988
  Copyright terms: Public domain W3C validator