MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1i13 Structured version   Visualization version   GIF version

Theorem a1i13 27
Description: Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)
Hypothesis
Ref Expression
a1i13.1 (𝜓𝜃)
Assertion
Ref Expression
a1i13 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem a1i13
StepHypRef Expression
1 a1i13.1 . . 3 (𝜓𝜃)
21a1d 25 . 2 (𝜓 → (𝜒𝜃))
32a1i 11 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  propeqop  5468  seqshft2  13943  seqsplit  13950  resqrex  15144  2mulprm  16577  comppfsc  22906  filconn  23257  sinq12ge0  25888  usgr2pth  28761  elwspths2on  28954  frgr3vlem1  29266  3vfriswmgrlem  29270  onsupnmax  41609  cantnfresb  41706  dflim5  41711
  Copyright terms: Public domain W3C validator