Theorem biimpac 503

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 239	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 445	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

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:  gencbvex2  3251  2reu5  3416  ifpprsnss  4299  poltletr  5528  ordnbtwn  5816  ordnbtwnOLD  5817  tz6.12-1  6210  nfunsn  6225  funopsn  6413  onsucuni2  7034  smo11  7461  omlimcl  7658  omxpenlem  8061  fodomr  8111  fodomfib  8240  r1val1  8649  alephval3  8933  dfac5lem4  8949  dfac5  8951  axdc4lem  9277  fodomb  9348  distrlem1pr  9847  map2psrpr  9931  supsrlem  9932  eqle  10139  swrd0  13434  reuccats1lem  13479  repswswrd  13531  cshwidxmod  13549  rtrclind  13805  sumz  14453  prod1  14674  divalglem8  15123  flodddiv4  15137  pospo  16973  mgm2nsgrplem2  17406  lsmcv  19141  opsrtoslem1  19484  psrbagfsupp  19509  madugsum  20449  hauscmplem  21209  bwth  21213  ptbasfi  21384  hmphindis  21600  fbncp  21643  fgcl  21682  fixufil  21726  uffixfr  21727  mbfima  23399  mbfimaicc  23400  ig1pdvds  23936  zabsle1  25021  tgldimor  25397  ax5seglem4  25812  axcontlem2  25845  axcontlem4  25847  nbgrval  26234  cusgrfi  26354  fusgrregdegfi  26465  rusgr1vtxlem  26483  wlkiswwlksupgr2  26763  elwwlks2ons3  26848  eucrctshift  27103  numclwlk1lem2f1  27227  spansncvi  28511  eigposi  28695  pjnormssi  29027  sumdmdlem  29277  rhmdvdsr  29818  bnj168  30798  bnj521  30805  bnj964  31013  bnj966  31014  bnj1398  31102  cgrdegen  32111  btwnconn1lem11  32204  btwnconn1lem12  32205  btwnconn1lem14  32207  bj-elid3  33087  bj-ccinftydisj  33100  phpreu  33393  fin2so  33396  matunitlindflem2  33406  poimirlem26  33435  poimirlem28  33437  dvasin  33496  isbnd2  33582  atcvrj0  34714  paddasslem5  35110  pm13.13a  38608  iotavalb  38631  suctrALTcf  39158  suctrALTcfVD  39159  suctrALT3  39160  unisnALT  39162  2sb5ndALT  39168  xreqle  39534  supminfxr2  39699  fourierdlem40  40364  fourierdlem78  40401  2ffzoeq  41338  uspgropssxp  41752  uspgrsprfo  41756  difmodm1lt  42317  nn0sumshdiglemA  42413