Theorem 3impia 1179

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

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1176	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  mopick2  2083  3gencl  2723  mob2  2868  moi  2871  reupick3  3366  disjne  3421  disji2  3930  tz7.2  4284  funopg  5165  fvun1  5495  fvopab6  5525  isores3  5724  ovmpt4g  5901  ovmpos  5902  ov2gf  5903  ofrval  6000  poxp  6137  smoel  6205  tfr1onlemaccex  6253  tfrcllemaccex  6266  nnaass  6389  qsel  6514  xpdom3m  6736  phpm  6767  ctssdc  7006  mkvprop  7040  prarloclem3  7329  aptisr  7611  axpre-apti  7717  axapti  7859  addn0nid  8160  divvalap  8458  letrp1  8630  p1le  8631  zextle  9166  zextlt  9167  btwnnz  9169  gtndiv  9170  uzind2  9187  fzind  9190  iccleub  9744  uzsubsubfz  9858  elfz0fzfz0  9934  difelfznle  9943  elfzo0le  9993  fzonmapblen  9995  fzofzim  9996  fzosplitprm1  10042  rebtwn2zlemstep  10061  qbtwnxr  10066  expcl2lemap  10336  expclzaplem  10348  expnegzap  10358  leexp2r  10378  expnbnd  10446  bcval4  10530  bccmpl  10532  absexpzap  10884  divalgb  11658  ndvdssub  11663  dvdsgcd  11736  dfgcd2  11738  rplpwr  11751  lcmgcdlem  11794  coprmdvds1  11808  qredeq  11813  prmdvdsexpr  11864  elrestr  12167  mopni  12690  sincosq1lem  12954  logbgcd1irr  13092