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  3103  gencbvex2  3521  2reu5  3741  ifpprsnss  4740  dfiun2g  5006  poltletr  6121  ordnbtwn  6447  tz6.12-1OLD  6900  funopsn  7138  onsucuni2  7828  1stconst  8099  2ndconst  8100  smo11  8378  omlimcl  8590  omxpenlem  9087  fodomr  9142  f1oenfirn  9194  f1domfi  9195  fodomfib  9341  fodomfibOLD  9343  infsupprpr  9518  r1val1  9800  alephval3  10124  dfac5lem4  10140  dfac5lem4OLD  10142  dfac5  10143  axdc4lem  10469  fodomb  10540  distrlem1pr  11039  map2psrpr  11124  supsrlem  11125  eqle  11337  swrd0  14676  repswswrd  14802  cshwidxmod  14821  rtrclind  15084  sumz  15738  prod1  15960  divalglem8  16419  flodddiv4  16434  pospo  18355  mgm2nsgrplem2  18897  eqg0subg  19179  rhmdvdsr  20468  lsmcv  21102  sraring  21144  opsrtoslem1  22013  madugsum  22581  hauscmplem  23344  bwth  23348  ptbasfi  23519  hmphindis  23735  fbncp  23777  fgcl  23816  fixufil  23860  uffixfr  23861  mbfima  25583  mbfimaicc  25584  ig1pdvds  26137  zabsle1  27259  tgldimor  28481  ax5seglem4  28911  axcontlem2  28944  axcontlem4  28946  nbgrval  29315  cusgrfi  29438  fusgrregdegfi  29549  rusgr1vtxlem  29567  wlkiswwlksupgr2  29859  elwwlks2ons3  29937  clwwlknonwwlknonb  30087  eucrctshift  30224  spansncvi  31633  eigposi  31817  pjnormssi  32149  sumdmdlem  32399  tngdim  33653  bnj168  34761  bnj964  34974  bnj966  34975  bnj1398  35065  fnrelpredd  35120  lfuhgr3  35142  acycgrislfgr  35174  cgrdegen  36022  btwnconn1lem11  36115  btwnconn1lem12  36116  btwnconn1lem14  36118  bj-opelidb1  37171  bj-inexeqex  37172  bj-idreseqb  37181  bj-ideqg1ALT  37183  bj-ccinftydisj  37231  phpreu  37628  fin2so  37631  matunitlindflem2  37641  poimirlem26  37670  poimirlem28  37672  dvasin  37728  isbnd2  37807  atcvrj0  39447  paddasslem5  39843  expeq1d  42373  pm13.13a  44431  iotavalb  44454  suctrALTcf  44946  suctrALTcfVD  44947  suctrALT3  44948  unisnALT  44950  2sb5ndALT  44956  xreqle  45346  supminfxr2  45496  fourierdlem40  46176  fourierdlem78  46213  tz6.12-afv2  47269  afv2fv0  47294  2ffzoeq  47356  clnbgrval  47836  dfsclnbgr6  47871  uspgrlimlem1  48000  uspgropssxp  48119  uspgrsprfo  48123  difmodm1lt  48502  nn0sumshdiglemA  48599  itscnhlc0yqe  48739