Theorem mp3an12i 1382

Description: mp3an 1378 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an12i.1	⊢ 𝜑
mp3an12i.2	⊢ 𝜓
mp3an12i.3	⊢ (𝜒 → 𝜃)
mp3an12i.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
mp3an12i	⊢ (𝜒 → 𝜏)

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 ⊢ (𝜒 → 𝜃)
2		mp3an12i.1	. . 3 ⊢ 𝜑
3		mp3an12i.2	. . 3 ⊢ 𝜓
4		mp3an12i.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	mp3an12 1368	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 14	1 ⊢ (𝜒 → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

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

This theorem is used by:  funopsn  5891  map1  7101  exmidpw2en  7219  2omapen  7319  suplocsrlempr  8174  hashf1lem1  11285  geo2lim  12283  fprodge0  12404  fprodge1  12406  3dvds  12631  oddp1d2  12657  bezoutlema  12776  bezoutlemb  12777  pythagtriplem1  13044  exmidunben  13317  psrelbas  15066  psraddcl  15071  psr0cl  15072  psr0lid  15073  psrnegcl  15074  psrlinv  15075  psrgrp  15076  psr1clfi  15079  mplsubgfilemcl  15090  ismet  15445  isxmet  15446  dvidrelem  15793  coseq0negpitopi  15937  cosq34lt1  15951  cos02pilt1  15952  logdivlti  15982  1sgm2ppw  16109  lgseisenlem1  16189  lgseisen  16193  lgsquad3  16203  m1lgs  16204  pw1mapen  17026