Theorem 3impia 1226

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 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1219	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  mopick2  2163  3gencl  2837  mob2  2986  moi  2989  reupick3  3492  disjne  3548  elpr2elpr  3859  disji2  4080  tz7.2  4451  funopg  5360  fvun1  5712  fvopab6  5743  isores3  5956  ovmpt4g  6144  ovmpos  6145  ov2gf  6146  ofrval  6246  poxp  6397  smoel  6466  tfr1onlemaccex  6514  tfrcllemaccex  6527  nnaass  6653  qsel  6781  xpdom3m  7018  phpm  7052  ctssdc  7312  mkvprop  7357  prarloclem3  7717  aptisr  7999  axpre-apti  8105  axapti  8250  addn0nid  8553  divvalap  8854  letrp1  9028  p1le  9029  zextle  9571  zextlt  9572  btwnnz  9574  gtndiv  9575  uzind2  9592  fzind  9595  iccleub  10166  uzsubsubfz  10282  elfz0fzfz0  10361  difelfznle  10370  elfzo0le  10425  fzonmapblen  10427  fzofzim  10428  fzosplitprm1  10481  rebtwn2zlemstep  10513  qbtwnxr  10518  icogelb  10526  expcl2lemap  10814  expclzaplem  10826  expnegzap  10836  leexp2r  10856  expnbnd  10926  bcval4  11015  bccmpl  11017  elovmpowrd  11159  ccatval2  11179  ccatrcl1  11195  wrdl1s1  11211  ccat2s1fvwd  11228  swrdsb0eq  11250  swrdccatin1  11310  pfxccatpfx2  11322  absexpzap  11658  divalgb  12504  ndvdssub  12509  dvdsgcd  12601  dfgcd2  12603  rplpwr  12616  nnmindc  12623  lcmgcdlem  12667  coprmdvds1  12681  qredeq  12686  prmdvdsexpr  12740  nnnn0modprm0  12846  pcexp  12900  difsqpwdvds  12929  prmpwdvds  12946  elrestr  13348  isnmgm  13461  grpasscan1  13664  grpinvnz  13672  mulgneg2  13761  dvdsrmul1  14135  dvdsunit  14145  lmodlema  14325  mopni  15225  sincosq1lem  15568  rpcxpmul2  15656  logbgcd1irr  15710  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem4  15812  2lgsoddprmlem3  15859  uhgredgrnv  16008  usgredg4  16085  usgr2v1e2w  16116  uspgr2wlkeqi  16237  eupth2lem3lem4fi  16343