Theorem biimp3a 1471

Description: Infer implication from a logical equivalence. Similar to biimpa 476. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
biimp3a.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
biimp3a	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem biimp3a

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	biimpa 476	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1109	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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  df-3an 1088

This theorem is referenced by:  onomeneq  9138  nn0addge1  12449  nn0addge2  12450  nn0sub2  12556  eluzp1p1  12782  uznn0sub  12793  uzinfi  12848  iocssre  13349  icossre  13350  iccssre  13351  lincmb01cmp  13417  iccf1o  13418  fzosplitprm1  13699  subfzo0  13711  modfzo0difsn  13869  hashprb  14323  pfxpfx  14633  eflt  16045  fldivndvdslt  16346  prmdiv  16715  hashgcdlem  16718  vfermltl  16732  coprimeprodsq  16739  pythagtrip  16765  difsqpwdvds  16818  cshwshashlem2  17027  odinf  19461  odcl2  19463  rnghmresel  20524  rhmresel  20553  slesolex  22586  tgtop11  22886  restntr  23086  hauscmplem  23310  icchmeo  24855  icchmeoOLD  24856  pi1xfr  24972  sinq12gt0  26433  tanord1  26463  gausslemma2dlem1a  27293  sltn0  27839  onltn0s  28272  pw2cut  28367  axsegconlem6  28886  lfuhgr1v0e  29218  crctcshwlkn0lem6  29779  crctcshwlkn0lem7  29780  clwlkclwwlkf1lem2  29968  s2elclwwlknon2  30067  eucrctshift  30206  eucrct2eupth  30208  nv1  30638  lnolin  30717  br8d  32574  fzm1ne1  32750  ismntd  32945  mntf  32946  cycpmco2lem6  33092  ballotlemfc0  34480  ballotlemfcc  34481  ballotlemrv2  34509  fisshasheq  35107  br8  35748  br6  35749  br4  35750  bj-imdiridlem  37178  ismtyima  37802  ismtybndlem  37805  ghomlinOLD  37887  ghomidOLD  37888  cvrcmp2  39282  atcvrj2  39432  1cvratex  39472  lplnric  39551  lplnri1  39552  lnatexN  39778  ltrnateq  40180  ltrnatneq  40181  cdleme46f2g2  40492  cdleme46f2g1  40493  dibelval1st  41148  dibelval2nd  41151  dicelval1sta  41186  hlhilphllem  41958  jm2.17b  42954  bi123impia  44484  sineq0ALT  44930  eliccre  45506  ioomidp  45515  smfinflem  46818  submodlt  47354  iccpartiltu  47426  goldbachthlem1  47549  evengpop3  47802  gpgcubic  48083  gpg5nbgr3star  48085  itcovalsuc  48672