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  3550  onomeneq  9201  nn0addge1  12561  nn0addge2  12562  nn0sub2  12669  eluzp1p1  12902  uznn0sub  12909  uzinfi  12964  iocssre  13466  icossre  13467  iccssre  13468  lincmb01cmp  13534  iccf1o  13535  fzosplitprm1  13820  subfzo0  13835  modfzo0difsn  13993  hashprb  14447  pfxpfx  14763  eflt  16191  fldivndvdslt  16492  prmdiv  16862  hashgcdlem  16865  vfermltl  16879  coprimeprodsq  16886  pythagtrip  16912  difsqpwdvds  16965  cshwshashlem2  17174  odinf  19657  odcl2  19659  rnghmresel  20749  rhmresel  20778  slesolex  22869  tgtop11  23169  restntr  23369  hauscmplem  23593  icchmeo  25131  pi1xfr  25245  sinq12gt0  26703  tanord1  26733  gausslemma2dlem1a  27560  ltsn0  28130  onltn0s  28582  pw2cut  28684  axsegconlem6  29303  lfuhgr1v0e  29638  crctcshwlkn0lem6  30207  crctcshwlkn0lem7  30208  clwlkclwwlkf1lem2  30399  s2elclwwlknon2  30498  eucrctshift  30641  eucrct2eupth  30643  nv1  31074  lnolin  31153  br8d  33000  fzm1ne1  33179  ismntd  33344  mntf  33345  cycpmco2lem6  33491  ballotlemfc0  34924  ballotlemfcc  34925  ballotlemrv2  34953  fisshasheq  35637  br8  36261  br6  36262  br4  36263  cgsex2gd  37814  bj-imdiridlem  37862  ismtyima  38487  ismtybndlem  38490  ghomlinOLD  38572  ghomidOLD  38573  cvrcmp2  40091  atcvrj2  40240  1cvratex  40280  lplnric  40359  lplnri1  40360  lnatexN  40586  ltrnateq  40988  ltrnatneq  40989  cdleme46f2g2  41300  cdleme46f2g1  41301  dibelval1st  41956  dibelval2nd  41959  dicelval1sta  41994  hlhilphllem  42766  jm2.17b  43721  bi123impia  45232  sineq0ALT  45678  eliccre  46254  ioomidp  46263  smfinflem  47564  submodlt  48126  muldvdsfacgt  48156  iccpartiltu  48204  goldbachthlem1  48330  evengpop3  48596  gpgcubic  48877  gpg5nbgr3star  48879  itcovalsuc  49480