Theorem 3expib 1120

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1117	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 410	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anidm12  1417  mob  3655  eqbrrdva  5775  fcoOLD  6621  f1oiso2  7216  frxp  7951  onfununi  8156  smoel2  8178  smoiso2  8184  3ecoptocl  8572  ssfi  8921  f1domfi  8932  dffi2  9143  elfiun  9150  dif1card  9750  infxpenlem  9753  cfeq0  9996  cfsuc  9997  cfflb  9999  cfslb2n  10008  cofsmo  10009  domtriomlem  10182  axdc3lem4  10193  axdc4lem  10195  ttukey2g  10256  tskxpss  10512  grudomon  10557  elnpi  10728  dedekind  11121  nn0n0n1ge2b  12284  fzind  12401  suprzcl2  12660  icoshft  13187  fzen  13255  hashgt23el  14120  hashbclem  14145  seqcoll  14159  relexpsucl  14723  relexpsucr  14724  relexpfld  14741  shftuz  14761  mulgcd  16237  algcvga  16265  lcmneg  16289  ressbas  16928  ressbasOLD  16929  resseqnbas  16932  resslemOLD  16933  ressress  16939  psss  18279  tsrlemax  18285  isnmgm  18311  gsummgmpropd  18346  iscmnd  19380  ring1ne0  19811  unitmulclb  19888  isdrngd  19997  issrngd  20102  rmodislmodlem  20171  rmodislmod  20172  rmodislmodOLD  20173  abvn0b  20554  isphld  20840  mpfaddcl  21296  mpfmulcl  21297  pf1addcl  21500  pf1mulcl  21501  fitop  22030  hausnei2  22485  ordtt1  22511  locfincmp  22658  basqtop  22843  filfi  22991  fgcl  23010  neifil  23012  filuni  23017  cnextcn  23199  prdsmet  23504  blssps  23558  blss  23559  metcnp3  23677  hlhil  24588  volsup2  24750  sincosq1sgn  25636  sincosq2sgn  25637  sincosq3sgn  25638  sincosq4sgn  25639  sinq12ge0  25646  bcmono  26406  iswlkg  27961  umgrwwlks2on  28301  clwlkclwwlkfo  28352  3cyclfrgrrn1  28628  grpodivf  28879  ipf  29054  shintcli  29670  spanuni  29885  adjadj  30277  unopadj2  30279  hmopadj  30280  hmopbdoptHIL  30329  resvsca  31508  resvlem  31509  resvlemOLD  31510  submateq  31738  esumcocn  32027  bnj1379  32789  bnj571  32865  bnj594  32871  bnj580  32872  bnj600  32878  bnj1189  32968  bnj1321  32986  bnj1384  32991  f1resrcmplf1dlem  33037  hashfundm  33053  cplgredgex  33061  cusgr3cyclex  33077  loop1cycl  33078  umgr2cycllem  33081  umgr2cycl  33082  acycgr2v  33091  cusgracyclt3v  33097  climuzcnv  33608  fness  34517  bj-idreseq  35312  bj-imdiridlem  35335  neificl  35890  metf1o  35892  isismty  35938  ismtybndlem  35943  ablo4pnp  36017  divrngcl  36094  keridl  36169  prnc  36204  lsmsatcv  37003  llncvrlpln2  37550  lplncvrlvol2  37608  linepsubN  37745  pmapsub  37761  dalawlem10  37873  dalawlem13  37876  dalawlem14  37877  dalaw  37879  diaf11N  39042  dibf11N  39154  ismrcd1  40500  ismrcd2  40501  mzpincl  40536  mzpadd  40540  mzpmul  40541  pellfundge  40684  imasgim  40905  sqrtcval  41202  stoweidlem2  43497  stoweidlem17  43512  imaelsetpreimafv  44799  opnneir  46152  i0oii  46165  io1ii  46166