Theorem biimp3a 1386

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  nnawordex  6792  div2subap  9157  nn0addge1  9588  nn0addge2  9589  nn0sub2  9697  eluzp1p1  9927  uznn0sub  9933  iocssre  10334  icossre  10335  iccssre  10336  lincmb01cmp  10384  iccf1o  10386  fzosplitprm1  10631  subfzo0  10639  modfzo0difsn  10810  pfxpfx  11458  efltim  12443  fldivndvdslt  12682  prmdiv  12991  hashgcdlem  12994  vfermltl  13008  coprimeprodsq  13014  pythagtrip  13040  difsqpwdvds  13095  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemrv2  13243  tgtop11  15100  sinq12gt0  15854  gausslemma2dlem1a  16091  s2elclwwlknon2  16591