Theorem mp3an12i 1375

Description: mp3an 1371 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 1361	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 14	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  funopsn  5819  map1  6973  exmidpw2en  7085  suplocsrlempr  8005  geo2lim  12043  fprodge0  12164  fprodge1  12166  3dvds  12391  oddp1d2  12417  bezoutlema  12536  bezoutlemb  12537  pythagtriplem1  12804  exmidunben  13013  psrelbas  14655  psraddcl  14660  psr0cl  14661  psr0lid  14662  psrnegcl  14663  psrlinv  14664  psrgrp  14665  psr1clfi  14668  mplsubgfilemcl  14679  ismet  15034  isxmet  15035  dvidrelem  15382  coseq0negpitopi  15526  cosq34lt1  15540  cos02pilt1  15541  logdivlti  15571  1sgm2ppw  15685  lgseisenlem1  15765  lgseisen  15769  lgsquad3  15779  m1lgs  15780  2omapen  16447  pw1mapen  16449