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  3122  gencbvex2  3554  2reu5  3780  ifpprsnss  4789  dfiun2g  5053  poltletr  6164  ordnbtwn  6488  tz6.12-1OLD  6944  funopsn  7182  onsucuni2  7870  1stconst  8141  2ndconst  8142  smo11  8420  omlimcl  8634  omxpenlem  9139  fodomr  9194  f1oenfirn  9246  f1domfi  9247  fodomfib  9397  fodomfibOLD  9399  infsupprpr  9573  r1val1  9855  alephval3  10179  dfac5lem4  10195  dfac5lem4OLD  10197  dfac5  10198  axdc4lem  10524  fodomb  10595  distrlem1pr  11094  map2psrpr  11179  supsrlem  11180  eqle  11392  swrd0  14706  repswswrd  14832  cshwidxmod  14851  rtrclind  15114  sumz  15770  prod1  15992  divalglem8  16448  flodddiv4  16461  pospo  18415  mgm2nsgrplem2  18954  eqg0subg  19236  rhmdvdsr  20534  lsmcv  21166  sraring  21216  opsrtoslem1  22102  madugsum  22670  hauscmplem  23435  bwth  23439  ptbasfi  23610  hmphindis  23826  fbncp  23868  fgcl  23907  fixufil  23951  uffixfr  23952  mbfima  25684  mbfimaicc  25685  ig1pdvds  26239  zabsle1  27358  tgldimor  28528  ax5seglem4  28965  axcontlem2  28998  axcontlem4  29000  nbgrval  29371  cusgrfi  29494  fusgrregdegfi  29605  rusgr1vtxlem  29623  wlkiswwlksupgr2  29910  elwwlks2ons3  29988  clwwlknonwwlknonb  30138  eucrctshift  30275  spansncvi  31684  eigposi  31868  pjnormssi  32200  sumdmdlem  32450  tngdim  33626  bnj168  34706  bnj964  34919  bnj966  34920  bnj1398  35010  fnrelpredd  35065  lfuhgr3  35087  acycgrislfgr  35120  cgrdegen  35968  btwnconn1lem11  36061  btwnconn1lem12  36062  btwnconn1lem14  36064  bj-opelidb1  37119  bj-inexeqex  37120  bj-idreseqb  37129  bj-ideqg1ALT  37131  bj-ccinftydisj  37179  phpreu  37564  fin2so  37567  matunitlindflem2  37577  poimirlem26  37606  poimirlem28  37608  dvasin  37664  isbnd2  37743  atcvrj0  39385  paddasslem5  39781  expeq1d  42311  pm13.13a  44376  iotavalb  44399  suctrALTcf  44893  suctrALTcfVD  44894  suctrALT3  44895  unisnALT  44897  2sb5ndALT  44903  xreqle  45233  supminfxr2  45384  fourierdlem40  46068  fourierdlem78  46105  tz6.12-afv2  47155  afv2fv0  47180  2ffzoeq  47242  clnbgrval  47696  dfsclnbgr6  47730  uspgrlimlem1  47812  uspgropssxp  47867  uspgrsprfo  47871  difmodm1lt  48256  nn0sumshdiglemA  48353  itscnhlc0yqe  48493