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  3543  onomeneq  9208  nn0addge1  12574  nn0addge2  12575  nn0sub2  12682  eluzp1p1  12915  uznn0sub  12922  uzinfi  12977  iocssre  13480  icossre  13481  iccssre  13482  lincmb01cmp  13548  iccf1o  13549  fzosplitprm1  13834  subfzo0  13849  modfzo0difsn  14007  hashprb  14461  pfxpfx  14777  eflt  16205  fldivndvdslt  16506  prmdiv  16876  hashgcdlem  16879  vfermltl  16893  coprimeprodsq  16900  pythagtrip  16926  difsqpwdvds  16979  cshwshashlem2  17188  odinf  19690  odcl2  19692  rnghmresel  20782  rhmresel  20811  slesolex  22907  tgtop11  23207  restntr  23407  hauscmplem  23631  icchmeo  25169  pi1xfr  25283  sinq12gt0  26745  tanord1  26774  gausslemma2dlem1a  27601  ltsn0  28171  onltn0s  28623  pw2cut  28725  axsegconlem6  29379  lfuhgr1v0e  29714  crctcshwlkn0lem6  30283  crctcshwlkn0lem7  30284  clwlkclwwlkf1lem2  30475  s2elclwwlknon2  30574  eucrctshift  30723  eucrct2eupth  30725  nv1  31156  lnolin  31235  br8d  33081  fzm1ne1  33259  ismntd  33424  mntf  33425  cycpmco2lem6  33571  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemrv2  35033  fisshasheq  35717  br8  36335  br6  36336  br4  36337  cgsex2gd  37889  bj-imdiridlem  37937  ismtyima  38553  ismtybndlem  38556  ghomlinOLD  38638  ghomidOLD  38639  cvrcmp2  40157  atcvrj2  40306  1cvratex  40346  lplnric  40425  lplnri1  40426  lnatexN  40652  ltrnateq  41054  ltrnatneq  41055  cdleme46f2g2  41366  cdleme46f2g1  41367  dibelval1st  42022  dibelval2nd  42025  dicelval1sta  42060  hlhilphllem  42832  jm2.17b  43802  bi123impia  45313  sineq0ALT  45759  eliccre  46335  ioomidp  46344  smfinflem  47645  submodlt  48244  muldvdsfacgt  48274  iccpartiltu  48322  goldbachthlem1  48448  evengpop3  48714  gpgcubic  48995  gpg5nbgr3star  48997  itcovalsuc  49597