Theorem exbiri 626

Description: Inference form of exbir 36804. This proof is exbiriVD 37224 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 487	. 2 |- ( ( ( ph /\ ps ) /\ th ) -> ch )
3	2	exp31 607	1 |- ( ph -> ( ps -> ( th -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  biimp3ar  1365  eqrdavOLD  2421  tfrlem9  7115  sbthlem1  7692  addcanpr  9479  axpre-sup  9601  lbreu  10564  zmax  11269  uzsubsubfz  11829  elfzodifsumelfzo  11987  swrdccatin12lem3  12849  cshwidxmod  12908  prmgaplem6  15026  ucnima  21295  usgraidx2vlem2  25118  wwlkextwrd  25455  numclwlk1lem2f1  25821  mdslmd1lem1  27977  mdslmd1lem2  27978  dfon2  30446  cgrextend  30781  brsegle  30881  finxpsuclem  31754  poimirlem18  31923  poimirlem21  31926  brabg2  32007  iccelpart  38618  ralxfrd2  38873  usgridx2vlem2  39108