Theorem 3impib 1232

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
3impib	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 258	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1224	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ 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:  mob  3008  eqreu  3018  iotam  5372  funimaexglem  5467  ssimaexg  5768  funopdmsn  5898  rbropap  6518  dfsmo2  6562  3ecoptocl  6902  distrnq0  7833  addassnq0  7836  uzind  9769  fzind  9773  fnn0ind  9774  xltnegi  10255  facwordi  11201  shftvalg  11624  shftval4g  11625  mulgcd  12819  coprmdvds1  12895  pcfac  13159  mgmcl  13739  mhmlin  13834  mhmmulg  14026  issubg2m  14052  nsgbi  14067  gsumcom2fi  14276  srgmulgass  14401  dvdsrtr  14518  issubrng2  14628  issubrg2  14659  domnmuln0  14692  inopn  15241  basis1  15285  cnmpt2t  15531  cnmpt22  15532  cnmptcom  15536  xmeteq0  15597  sincosq1sgn  16065  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  speano5  17187