Theorem exbiri 622

Description: Inference form of exbir 31509. This proof is exbiriVD 31945 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)

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	biimpar 485	. 2 |- ( ( ( ph /\ ps ) /\ th ) -> ch )
3	2	exp31 604	1 |- ( ph -> ( ps -> ( th -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  biimp3ar  1320  eqrdavOLD  2453  tfrlem9  6957  sbthlem1  7534  addcanpr  9330  axpre-sup  9451  lbreu  10395  zmax  11065  uzsubsubfz  11592  elfzodifsumelfzo  11725  swrdccatin12lem3  12503  cshwidxmod  12562  ucnima  19998  usgraidx2vlem2  23489  mdslmd1lem1  25908  mdslmd1lem2  25909  dfon2  27772  cgrextend  28206  brsegle  28306  brabg2  28780  ralxfrd2  30308  elfzom1elp1fzo  30389  wwlkextwrd  30531  numclwlk1lem2f1  30858