Theorem 3expib 1128

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anidm12  1427  mob  3665  dfss2  3908  eqbrrdva  5818  f1oiso2  7303  frxp  8073  onfununi  8278  smoel2  8300  smoiso2  8306  3ecoptocl  8753  ssfi  9104  f1domfi  9112  rex2dom  9160  fodomfib  9236  dffi2  9333  elfiun  9340  dif1card  9930  infxpenlem  9933  cfeq0  10176  cfsuc  10177  cfflb  10179  cfslb2n  10188  cofsmo  10189  domtriomlem  10362  axdc3lem4  10373  axdc4lem  10375  ttukey2g  10436  tskxpss  10693  grudomon  10738  elnpi  10909  dedekind  11307  nn0n0n1ge2b  12504  fzind  12625  suprzcl2  12886  icoshft  13424  fzen  13493  hashgt23el  14384  hashfundm  14402  hashbclem  14412  seqcoll  14424  relexpsucl  14991  relexpsucr  14992  relexpfld  15009  shftuz  15029  mulgcd  16515  algcvga  16546  lcmneg  16570  ressbas  17204  resseqnbas  17210  ressress  17215  psss  18544  tsrlemax  18550  isnmgm  18610  gsummgmpropd  18647  issgrpd  18696  iscmnd  19767  ring1ne0  20278  unitmulclb  20359  isdrngd  20744  isdrngdOLD  20746  abvn0b  20815  issrngd  20834  rmodislmodlem  20926  rmodislmod  20927  isphld  21636  mpfaddcl  22096  mpfmulcl  22097  pf1addcl  22346  pf1mulcl  22347  fitop  22890  hausnei2  23343  ordtt1  23369  locfincmp  23516  basqtop  23701  filfi  23849  fgcl  23868  neifil  23870  filuni  23875  cnextcn  24057  prdsmet  24360  blssps  24414  blss  24415  metcnp3  24530  hlhil  25435  volsup2  25597  sincosq1sgn  26487  sincosq2sgn  26488  sincosq3sgn  26489  sincosq4sgn  26490  sinq12ge0  26497  bcmono  27265  n0cutlt  28376  bdayfin  28504  iswlkg  29707  usgrwwlks2on  30051  umgrwwlks2on  30052  clwlkclwwlkfo  30104  3cyclfrgrrn1  30380  grpodivf  30634  ipf  30809  shintcli  31425  spanuni  31640  adjadj  32032  unopadj2  32034  hmopadj  32035  hmopbdoptHIL  32084  resvsca  33422  resvlem  33423  submateq  34000  esumcocn  34271  bnj1379  35019  bnj571  35095  bnj594  35101  bnj580  35102  bnj600  35108  bnj1189  35198  bnj1321  35216  bnj1384  35221  f1resrcmplf1dlem  35274  trssfir1om  35299  fineqvinfep  35313  trssfir1omregs  35324  cplgredgex  35356  cusgr3cyclex  35371  loop1cycl  35372  umgr2cycllem  35375  umgr2cycl  35376  acycgr2v  35385  cusgracyclt3v  35391  climuzcnv  35906  fness  36584  cgsex2gd  37504  bj-idreseq  37529  bj-imdiridlem  37552  neificl  38127  metf1o  38129  isismty  38175  ismtybndlem  38180  ablo4pnp  38254  divrngcl  38331  keridl  38406  prnc  38441  lsmsatcv  39509  llncvrlpln2  40056  lplncvrlvol2  40114  linepsubN  40251  pmapsub  40267  dalawlem10  40379  dalawlem13  40382  dalawlem14  40383  dalaw  40385  diaf11N  41548  dibf11N  41660  ismrcd1  43154  ismrcd2  43155  mzpincl  43190  mzpadd  43194  mzpmul  43195  pellfundge  43334  imasgim  43552  sqrtcval  44092  stoweidlem2  46452  stoweidlem17  46467  imaelsetpreimafv  47877  opnneir  49404  i0oii  49417  io1ii  49418