Theorem biimp3a 1472

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 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  vtoclegft  3532  onomeneq  9141  nn0addge1  12474  nn0addge2  12475  nn0sub2  12581  eluzp1p1  12807  uznn0sub  12814  uzinfi  12869  iocssre  13371  icossre  13372  iccssre  13373  lincmb01cmp  13439  iccf1o  13440  fzosplitprm1  13724  subfzo0  13738  modfzo0difsn  13896  hashprb  14350  pfxpfx  14661  eflt  16075  fldivndvdslt  16376  prmdiv  16746  hashgcdlem  16749  vfermltl  16763  coprimeprodsq  16770  pythagtrip  16796  difsqpwdvds  16849  cshwshashlem2  17058  odinf  19529  odcl2  19531  rnghmresel  20588  rhmresel  20617  slesolex  22657  tgtop11  22957  restntr  23157  hauscmplem  23381  icchmeo  24918  pi1xfr  25032  sinq12gt0  26484  tanord1  26514  gausslemma2dlem1a  27342  ltsn0  27912  onltn0s  28364  pw2cut  28466  axsegconlem6  29005  lfuhgr1v0e  29337  crctcshwlkn0lem6  29898  crctcshwlkn0lem7  29899  clwlkclwwlkf1lem2  30090  s2elclwwlknon2  30189  eucrctshift  30328  eucrct2eupth  30330  nv1  30761  lnolin  30840  br8d  32696  fzm1ne1  32876  ismntd  33059  mntf  33060  cycpmco2lem6  33207  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemrv2  34682  fisshasheq  35313  br8  35954  br6  35955  br4  35956  cgsex2gd  37467  bj-imdiridlem  37515  ismtyima  38138  ismtybndlem  38141  ghomlinOLD  38223  ghomidOLD  38224  cvrcmp2  39744  atcvrj2  39893  1cvratex  39933  lplnric  40012  lplnri1  40013  lnatexN  40239  ltrnateq  40641  ltrnatneq  40642  cdleme46f2g2  40953  cdleme46f2g1  40954  dibelval1st  41609  dibelval2nd  41612  dicelval1sta  41647  hlhilphllem  42419  jm2.17b  43407  bi123impia  44935  sineq0ALT  45381  eliccre  45953  ioomidp  45962  smfinflem  47263  submodlt  47816  muldvdsfacgt  47846  iccpartiltu  47894  goldbachthlem1  48020  evengpop3  48286  gpgcubic  48567  gpg5nbgr3star  48569  itcovalsuc  49155