Theorem biimp3a 1498

Description: Infer implication from a logical equivalence. Similar to biimpa 482. (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 482	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  vtoclegft  3544  onomeneq  9222  nn0addge1  12645  nn0addge2  12646  nn0sub2  12753  eluzp1p1  12986  uznn0sub  12993  uzinfi  13048  iocssre  13551  icossre  13552  iccssre  13553  lincmb01cmp  13619  iccf1o  13620  fzosplitprm1  13906  subfzo0  13921  modfzo0difsn  14079  hashprb  14534  pfxpfx  14850  eflt  16278  fldivndvdslt  16579  prmdiv  16955  hashgcdlem  16958  vfermltl  16972  coprimeprodsq  16979  pythagtrip  17005  difsqpwdvds  17058  cshwshashlem2  17267  odinf  19770  odcl2  19772  rnghmresel  20865  rhmresel  20894  slesolex  22993  tgtop11  23293  restntr  23493  hauscmplem  23717  icchmeo  25255  pi1xfr  25369  sinq12gt0  26829  tanord1  26858  gausslemma2dlem1a  27685  ltsn0  28285  onltn0s  28737  pw2cut  28839  axsegconlem6  29493  lfuhgr1v0e  29828  crctcshwlkn0lem6  30397  crctcshwlkn0lem7  30398  clwlkclwwlkf1lem2  30589  s2elclwwlknon2  30688  eucrctshift  30837  eucrct2eupth  30839  nv1  31270  lnolin  31349  br8d  33195  fzm1ne1  33373  ismntd  33538  mntf  33539  cycpmco2lem6  33685  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemrv2  35147  fisshasheq  35882  br8  36500  br6  36501  br4  36502  cgsex2gd  38038  bj-imdiridlem  38086  ismtyima  38717  ismtybndlem  38720  ghomlinOLD  38802  ghomidOLD  38803  cvrcmp2  40321  atcvrj2  40470  1cvratex  40510  lplnric  40589  lplnri1  40590  lnatexN  40816  ltrnateq  41218  ltrnatneq  41219  cdleme46f2g2  41530  cdleme46f2g1  41531  dibelval1st  42186  dibelval2nd  42189  dicelval1sta  42224  hlhilphllem  42996  jm2.17b  43947  bi123impia  45458  sineq0ALT  45904  eliccre  46486  ioomidp  46495  smfinflem  47796  submodlt  48395  muldvdsfacgt  48425  iccpartiltu  48473  goldbachthlem1  48599  evengpop3  48865  gpgcubic  49146  gpg5nbgr3star  49148  itcovalsuc  49748