Theorem exbiri 652

Description: Inference form of exbir 38684. This proof is exbiriVD 39089 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 502	. 2 |- ( ( ( ph /\ ps ) /\ th ) -> ch )
3	2	exp31 630	1 |- ( ph -> ( ps -> ( th -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  biimp3ar  1433  ralxfrd  4879  ralxfrd2  4884  tfrlem9  7481  sbthlem1  8070  addcanpr  9868  axpre-sup  9990  lbreu  10973  zmax  11785  uzsubsubfz  12363  elfzodifsumelfzo  12533  swrdccatin12lem3  13490  cshwidxmod  13549  prmgaplem6  15760  ucnima  22085  gausslemma2dlem1a  25090  usgredg2vlem2  26118  umgr2v2enb1  26422  wwlksnextwrd  26792  numclwlk1lem2f1  27227  mdslmd1lem1  29184  mdslmd1lem2  29185  dfon2  31697  cgrextend  32115  brsegle  32215  finxpsuclem  33234  poimirlem18  33427  poimirlem21  33430  brabg2  33510  iccelpart  41369