Theorem 3expib 1129

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 1126	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 412	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  3anidm12  1428  mob  3660  dfss2  3903  eqbrrdva  5814  f1oiso2  7300  frxp  8070  onfununi  8275  smoel2  8297  smoiso2  8303  3ecoptocl  8750  ssfi  9101  f1domfi  9109  rex2dom  9157  fodomfib  9233  dffi2  9330  elfiun  9337  dif1card  9927  infxpenlem  9930  cfeq0  10173  cfsuc  10174  cfflb  10176  cfslb2n  10185  cofsmo  10186  domtriomlem  10359  axdc3lem4  10370  axdc4lem  10372  ttukey2g  10433  tskxpss  10690  grudomon  10735  elnpi  10906  dedekind  11304  nn0n0n1ge2b  12501  fzind  12622  suprzcl2  12883  icoshft  13421  fzen  13490  hashgt23el  14381  hashfundm  14399  hashbclem  14409  seqcoll  14421  relexpsucl  14988  relexpsucr  14989  relexpfld  15006  shftuz  15026  mulgcd  16512  algcvga  16543  lcmneg  16567  ressbas  17201  resseqnbas  17207  ressress  17212  psss  18541  tsrlemax  18547  isnmgm  18607  gsummgmpropd  18644  issgrpd  18693  iscmnd  19764  ring1ne0  20275  unitmulclb  20356  isdrngd  20741  isdrngdOLD  20743  abvn0b  20812  issrngd  20831  rmodislmodlem  20923  rmodislmod  20924  isphld  21633  mpfaddcl  22093  mpfmulcl  22094  pf1addcl  22343  pf1mulcl  22344  fitop  22887  hausnei2  23340  ordtt1  23366  locfincmp  23513  basqtop  23698  filfi  23846  fgcl  23865  neifil  23867  filuni  23872  cnextcn  24054  prdsmet  24357  blssps  24411  blss  24412  metcnp3  24527  hlhil  25432  volsup2  25594  sincosq1sgn  26484  sincosq2sgn  26485  sincosq3sgn  26486  sincosq4sgn  26487  sinq12ge0  26494  bcmono  27262  n0cutlt  28373  bdayfin  28501  iswlkg  29704  usgrwwlks2on  30048  umgrwwlks2on  30049  clwlkclwwlkfo  30101  3cyclfrgrrn1  30377  grpodivf  30631  ipf  30806  shintcli  31422  spanuni  31637  adjadj  32029  unopadj2  32031  hmopadj  32032  hmopbdoptHIL  32081  resvsca  33419  resvlem  33420  submateq  34005  esumcocn  34276  bnj1379  35027  bnj571  35103  bnj594  35109  bnj580  35110  bnj600  35116  bnj1189  35206  bnj1321  35224  bnj1384  35229  f1resrcmplf1dlem  35282  trssfir1om  35307  fineqvinfep  35321  trssfir1omregs  35332  cplgredgex  35364  cusgr3cyclex  35379  loop1cycl  35380  umgr2cycllem  35383  umgr2cycl  35384  acycgr2v  35393  cusgracyclt3v  35399  climuzcnv  35914  fness  36592  cgsex2gd  37512  bj-idreseq  37537  bj-imdiridlem  37560  neificl  38135  metf1o  38137  isismty  38183  ismtybndlem  38188  ablo4pnp  38262  divrngcl  38339  keridl  38414  prnc  38449  lsmsatcv  39517  llncvrlpln2  40064  lplncvrlvol2  40122  linepsubN  40259  pmapsub  40275  dalawlem10  40387  dalawlem13  40390  dalawlem14  40391  dalaw  40393  diaf11N  41556  dibf11N  41668  ismrcd1  43162  ismrcd2  43163  mzpincl  43198  mzpadd  43202  mzpmul  43203  pellfundge  43342  imasgim  43560  sqrtcval  44100  stoweidlem2  46459  stoweidlem17  46474  imaelsetpreimafv  47884  opnneir  49411  i0oii  49424  io1ii  49425