Theorem 3impia 1190

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

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

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 970

This theorem is referenced by:  mopick2  2097  3gencl  2759  mob2  2905  moi  2908  reupick3  3406  disjne  3461  disji2  3974  tz7.2  4331  funopg  5221  fvun1  5551  fvopab6  5581  isores3  5782  ovmpt4g  5960  ovmpos  5961  ov2gf  5962  ofrval  6059  poxp  6196  smoel  6264  tfr1onlemaccex  6312  tfrcllemaccex  6325  nnaass  6449  qsel  6574  xpdom3m  6796  phpm  6827  ctssdc  7074  mkvprop  7118  prarloclem3  7434  aptisr  7716  axpre-apti  7822  axapti  7965  addn0nid  8268  divvalap  8566  letrp1  8739  p1le  8740  zextle  9278  zextlt  9279  btwnnz  9281  gtndiv  9282  uzind2  9299  fzind  9302  iccleub  9863  uzsubsubfz  9978  elfz0fzfz0  10057  difelfznle  10066  elfzo0le  10116  fzonmapblen  10118  fzofzim  10119  fzosplitprm1  10165  rebtwn2zlemstep  10184  qbtwnxr  10189  icogelb  10197  expcl2lemap  10463  expclzaplem  10475  expnegzap  10485  leexp2r  10505  expnbnd  10574  bcval4  10661  bccmpl  10663  absexpzap  11018  divalgb  11858  ndvdssub  11863  dvdsgcd  11941  dfgcd2  11943  rplpwr  11956  nnmindc  11963  lcmgcdlem  12005  coprmdvds1  12019  qredeq  12024  prmdvdsexpr  12078  nnnn0modprm0  12183  pcexp  12237  difsqpwdvds  12265  prmpwdvds  12281  elrestr  12559  mopni  13082  sincosq1lem  13346  logbgcd1irr  13485