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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  r19.29r  3113  gencbvex2  3534  2reu5  3753  ifpprsnss  4769  dfiun2g  5033  poltletr  6138  ordnbtwn  6462  tz6.12-1OLD  6921  funopsn  7157  onsucuni2  7837  1stconst  8105  2ndconst  8106  smo11  8384  omlimcl  8598  omxpenlem  9097  fodomr  9152  f1oenfirn  9207  f1domfi  9208  fodomfib  9350  infsupprpr  9527  r1val1  9809  alephval3  10133  dfac5lem4  10149  dfac5  10151  axdc4lem  10478  fodomb  10549  distrlem1pr  11048  map2psrpr  11133  supsrlem  11134  eqle  11346  swrd0  14640  repswswrd  14766  cshwidxmod  14785  rtrclind  15044  sumz  15700  prod1  15920  divalglem8  16376  flodddiv4  16389  pospo  18336  mgm2nsgrplem2  18870  eqg0subg  19150  rhmdvdsr  20446  lsmcv  21028  sraring  21078  psrbagfsuppOLD  21853  opsrtoslem1  21998  madugsum  22544  hauscmplem  23309  bwth  23313  ptbasfi  23484  hmphindis  23700  fbncp  23742  fgcl  23781  fixufil  23825  uffixfr  23826  mbfima  25558  mbfimaicc  25559  ig1pdvds  26113  zabsle1  27228  tgldimor  28305  ax5seglem4  28742  axcontlem2  28775  axcontlem4  28777  nbgrval  29148  cusgrfi  29271  fusgrregdegfi  29382  rusgr1vtxlem  29400  wlkiswwlksupgr2  29687  elwwlks2ons3  29765  clwwlknonwwlknonb  29915  eucrctshift  30052  spansncvi  31461  eigposi  31645  pjnormssi  31977  sumdmdlem  32227  tngdim  33307  bnj168  34361  bnj964  34574  bnj966  34575  bnj1398  34665  fnrelpredd  34712  lfuhgr3  34729  acycgrislfgr  34762  cgrdegen  35600  btwnconn1lem11  35693  btwnconn1lem12  35694  btwnconn1lem14  35696  bj-opelidb1  36632  bj-inexeqex  36633  bj-idreseqb  36642  bj-ideqg1ALT  36644  bj-ccinftydisj  36692  phpreu  37077  fin2so  37080  matunitlindflem2  37090  poimirlem26  37119  poimirlem28  37121  dvasin  37177  isbnd2  37256  atcvrj0  38901  paddasslem5  39297  pm13.13a  43844  iotavalb  43867  suctrALTcf  44361  suctrALTcfVD  44362  suctrALT3  44363  unisnALT  44365  2sb5ndALT  44371  xreqle  44700  supminfxr2  44851  fourierdlem40  45535  fourierdlem78  45572  tz6.12-afv2  46620  afv2fv0  46645  2ffzoeq  46708  uspgropssxp  47206  uspgrsprfo  47210  difmodm1lt  47595  nn0sumshdiglemA  47692  itscnhlc0yqe  47832