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  2121  hbim1OLD  2226  ralimia  2946  ceqsalgALT  3221  rspct  3292  elabgt  3335  fvmptt  6266  tfi  7015  fnfi  8198  finsschain  8233  ordiso2  8380  ordtypelem7  8389  dfom3  8504  infdiffi  8515  cantnfp1lem3  8537  cantnf  8550  r1ordg  8601  ttukeylem6  9296  fpwwe2lem8  9419  wunfi  9503  dfnn2  10993  trclfvcotr  13700  psgnunilem3  17856  pgpfac1  18419  fiuncmp  21147  filssufilg  21655  ufileu  21663  pjnormssi  28915  bnj1110  30811  waj-ax  32108  bj-sb  32372  bj-equsal1  32507  bj-equsal2  32508  rdgeqoa  32889  wl-mps  32961  refimssco  37433  atbiffatnnb  40413  elsetrecslem  41767
 Copyright terms: Public domain W3C validator