Theorem biimpac 478

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpac	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem biimpac

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpcd 249	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  r19.29r  3116  gencbvex2  3542  2reu5  3764  ifpprsnss  4764  dfiun2g  5030  poltletr  6152  ordnbtwn  6477  tz6.12-1OLD  6930  funopsn  7168  onsucuni2  7854  1stconst  8125  2ndconst  8126  smo11  8404  omlimcl  8616  omxpenlem  9113  fodomr  9168  f1oenfirn  9220  f1domfi  9221  fodomfib  9369  fodomfibOLD  9371  infsupprpr  9544  r1val1  9826  alephval3  10150  dfac5lem4  10166  dfac5lem4OLD  10168  dfac5  10169  axdc4lem  10495  fodomb  10566  distrlem1pr  11065  map2psrpr  11150  supsrlem  11151  eqle  11363  swrd0  14696  repswswrd  14822  cshwidxmod  14841  rtrclind  15104  sumz  15758  prod1  15980  divalglem8  16437  flodddiv4  16452  pospo  18390  mgm2nsgrplem2  18932  eqg0subg  19214  rhmdvdsr  20508  lsmcv  21143  sraring  21193  opsrtoslem1  22079  madugsum  22649  hauscmplem  23414  bwth  23418  ptbasfi  23589  hmphindis  23805  fbncp  23847  fgcl  23886  fixufil  23930  uffixfr  23931  mbfima  25665  mbfimaicc  25666  ig1pdvds  26219  zabsle1  27340  tgldimor  28510  ax5seglem4  28947  axcontlem2  28980  axcontlem4  28982  nbgrval  29353  cusgrfi  29476  fusgrregdegfi  29587  rusgr1vtxlem  29605  wlkiswwlksupgr2  29897  elwwlks2ons3  29975  clwwlknonwwlknonb  30125  eucrctshift  30262  spansncvi  31671  eigposi  31855  pjnormssi  32187  sumdmdlem  32437  tngdim  33664  bnj168  34744  bnj964  34957  bnj966  34958  bnj1398  35048  fnrelpredd  35103  lfuhgr3  35125  acycgrislfgr  35157  cgrdegen  36005  btwnconn1lem11  36098  btwnconn1lem12  36099  btwnconn1lem14  36101  bj-opelidb1  37154  bj-inexeqex  37155  bj-idreseqb  37164  bj-ideqg1ALT  37166  bj-ccinftydisj  37214  phpreu  37611  fin2so  37614  matunitlindflem2  37624  poimirlem26  37653  poimirlem28  37655  dvasin  37711  isbnd2  37790  atcvrj0  39430  paddasslem5  39826  expeq1d  42359  pm13.13a  44426  iotavalb  44449  suctrALTcf  44942  suctrALTcfVD  44943  suctrALT3  44944  unisnALT  44946  2sb5ndALT  44952  xreqle  45330  supminfxr2  45480  fourierdlem40  46162  fourierdlem78  46199  tz6.12-afv2  47252  afv2fv0  47277  2ffzoeq  47339  clnbgrval  47809  dfsclnbgr6  47844  uspgrlimlem1  47955  uspgropssxp  48060  uspgrsprfo  48064  difmodm1lt  48443  nn0sumshdiglemA  48540  itscnhlc0yqe  48680