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  5517  seqshft2  14066  seqsplit  14073  resqrex  15286  2mulprm  16727  comppfsc  23556  filconn  23907  sinq12ge0  26565  usgr2pth  29797  elwspths2on  29990  frgr3vlem1  30302  3vfriswmgrlem  30306  onsupnmax  43217  cantnfresb  43314  dflim5  43319
  Copyright terms: Public domain W3C validator