Theorem 3impia 1182

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  2089  3gencl  2746  mob2  2892  moi  2895  reupick3  3392  disjne  3447  disji2  3958  tz7.2  4314  funopg  5203  fvun1  5533  fvopab6  5563  isores3  5762  ovmpt4g  5940  ovmpos  5941  ov2gf  5942  ofrval  6039  poxp  6176  smoel  6244  tfr1onlemaccex  6292  tfrcllemaccex  6305  nnaass  6429  qsel  6554  xpdom3m  6776  phpm  6807  ctssdc  7051  mkvprop  7095  prarloclem3  7411  aptisr  7693  axpre-apti  7799  axapti  7942  addn0nid  8243  divvalap  8541  letrp1  8713  p1le  8714  zextle  9249  zextlt  9250  btwnnz  9252  gtndiv  9253  uzind2  9270  fzind  9273  iccleub  9828  uzsubsubfz  9942  elfz0fzfz0  10018  difelfznle  10027  elfzo0le  10077  fzonmapblen  10079  fzofzim  10080  fzosplitprm1  10126  rebtwn2zlemstep  10145  qbtwnxr  10150  icogelb  10158  expcl2lemap  10424  expclzaplem  10436  expnegzap  10446  leexp2r  10466  expnbnd  10534  bcval4  10619  bccmpl  10621  absexpzap  10973  divalgb  11808  ndvdssub  11813  dvdsgcd  11887  dfgcd2  11889  rplpwr  11902  lcmgcdlem  11945  coprmdvds1  11959  qredeq  11964  prmdvdsexpr  12015  elrestr  12330  mopni  12853  sincosq1lem  13117  logbgcd1irr  13255