Theorem 3impia 1141

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 1138	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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

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

This theorem is referenced by:  mopick2  2032  3gencl  2654  mob2  2796  moi  2799  reupick3  3285  disjne  3340  disji2  3844  tz7.2  4190  funopg  5061  fvun1  5383  fvopab6  5410  isores3  5608  ovmpt4g  5781  ovmpt2s  5782  ov2gf  5783  ofrval  5880  poxp  6011  smoel  6079  tfr1onlemaccex  6127  tfrcllemaccex  6140  nnaass  6260  qsel  6383  xpdom3m  6604  phpm  6635  prarloclem3  7117  aptisr  7385  axpre-apti  7481  axapti  7618  addn0nid  7913  divvalap  8202  letrp1  8370  p1le  8371  zextle  8898  zextlt  8899  btwnnz  8901  gtndiv  8902  uzind2  8919  fzind  8922  iccleub  9410  uzsubsubfz  9522  elfz0fzfz0  9598  difelfznle  9607  elfzo0le  9657  fzonmapblen  9659  fzofzim  9660  fzosplitprm1  9706  rebtwn2zlemstep  9725  qbtwnxr  9730  expcl2lemap  10028  expclzaplem  10040  expnegzap  10050  leexp2r  10070  expnbnd  10138  bcval4  10221  bccmpl  10223  absexpzap  10574  divalgb  11264  ndvdssub  11269  dvdsgcd  11340  dfgcd2  11342  rplpwr  11355  lcmgcdlem  11398  coprmdvds1  11412  qredeq  11417  prmdvdsexpr  11468  elrestr  11721