Theorem exbiri 421

Description: Inference form of exbir 1285. This proof is exbiriVD 16678 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
exbiri.1	|- ((ph /\ ps) -> (ch <-> th))

Assertion

Ref	Expression
exbiri	|- (ph -> (ps -> (th -> ch)))

Proof of Theorem exbiri

Step	Hyp	Ref	Expression
1		exbiri.1	. . 3 |- ((ph /\ ps) -> (ch <-> th))
2	1	ex 402	. 2 |- (ph -> (ps -> (ch <-> th)))
3		bi2 166	. 2 |- ((ch <-> th) -> (th -> ch))
4	2, 3	syl6 25	1 |- (ph -> (ps -> (th -> ch)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  eqrdav 1883  ordsssuc2OLD 3759  ralxfrd 3837  tfrlem9 5127  sbthlem1 5510  addcanpr 6304  lbreu 7254  uzwo5OLD 7423  zmax 7433  mulc1cncf 8541  metelcls 9243  cardennn 10171  mdslmd1lem1 11897  mdslmd1lem2 11898  fseq1cl 13619  dfon2 13858  brabg2 15681  enf1f1o 15720  addccncf 15883  sub1cncf 15885  sub2cncf 15886

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain