Theorem exbiri 622

Description: Inference form of exbir 32591. This proof is exbiriVD 33027 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  1329  eqrdavOLD  2466  tfrlem9  7064  sbthlem1  7637  addcanpr  9434  axpre-sup  9556  lbreu  10503  zmax  11189  uzsubsubfz  11717  elfzodifsumelfzo  11860  swrdccatin12lem3  12690  cshwidxmod  12749  ucnima  20629  usgraidx2vlem2  24183  wwlkextwrd  24519  numclwlk1lem2f1  24886  mdslmd1lem1  27035  mdslmd1lem2  27036  dfon2  29119  cgrextend  29553  brsegle  29653  brabg2  30101  ralxfrd2  32061