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  11299  geo2lim  12299  fprodge0  12420  fprodge1  12422  3dvds  12647  oddp1d2  12673  bezoutlema  12792  bezoutlemb  12793  pythagtriplem1  13064  exmidunben  13366  psrelbas  15115  psraddcl  15120  psr0cl  15121  psr0lid  15122  psrnegcl  15123  psrlinv  15124  psrgrp  15125  psr1clfi  15128  mplsubgfilemcl  15139  ismet  15494  isxmet  15495  dvidrelem  15842  coseq0negpitopi  15987  cosq34lt1  16001  cos02pilt1  16002  logdivlti  16033  1sgm2ppw  16190  ppiublem1  16192  lgseisenlem1  16287  lgseisen  16291  lgsquad3  16301  m1lgs  16302  pw1mapen  17124