Theorem exbiri 622

Description: Inference form of exbir 32952. This proof is exbiriVD 33387 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  1330  eqrdavOLD  2442  tfrlem9  7056  sbthlem1  7629  addcanpr  9427  axpre-sup  9549  lbreu  10499  zmax  11188  uzsubsubfz  11716  elfzodifsumelfzo  11861  swrdccatin12lem3  12694  cshwidxmod  12753  ucnima  20657  usgraidx2vlem2  24264  wwlkextwrd  24600  numclwlk1lem2f1  24966  mdslmd1lem1  27116  mdslmd1lem2  27117  dfon2  29199  cgrextend  29633  brsegle  29733  brabg2  30181  ralxfrd2  32141