Theorem 3expib 1122

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anidm12  1421  mob  3675  dfss2  3919  eqbrrdva  5818  f1oiso2  7298  frxp  8068  onfununi  8273  smoel2  8295  smoiso2  8301  3ecoptocl  8746  ssfi  9097  f1domfi  9105  rex2dom  9153  fodomfib  9229  dffi2  9326  elfiun  9333  dif1card  9920  infxpenlem  9923  cfeq0  10166  cfsuc  10167  cfflb  10169  cfslb2n  10178  cofsmo  10179  domtriomlem  10352  axdc3lem4  10363  axdc4lem  10365  ttukey2g  10426  tskxpss  10683  grudomon  10728  elnpi  10899  dedekind  11296  nn0n0n1ge2b  12470  fzind  12590  suprzcl2  12851  icoshft  13389  fzen  13457  hashgt23el  14347  hashfundm  14365  hashbclem  14375  seqcoll  14387  relexpsucl  14954  relexpsucr  14955  relexpfld  14972  shftuz  14992  mulgcd  16475  algcvga  16506  lcmneg  16530  ressbas  17163  resseqnbas  17169  ressress  17174  psss  18503  tsrlemax  18509  isnmgm  18569  gsummgmpropd  18606  issgrpd  18655  iscmnd  19723  ring1ne0  20234  unitmulclb  20317  isdrngd  20698  isdrngdOLD  20700  abvn0b  20769  issrngd  20788  rmodislmodlem  20880  rmodislmod  20881  isphld  21609  mpfaddcl  22068  mpfmulcl  22069  pf1addcl  22297  pf1mulcl  22298  fitop  22844  hausnei2  23297  ordtt1  23323  locfincmp  23470  basqtop  23655  filfi  23803  fgcl  23822  neifil  23824  filuni  23829  cnextcn  24011  prdsmet  24314  blssps  24368  blss  24369  metcnp3  24484  hlhil  25399  volsup2  25562  sincosq1sgn  26463  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  sinq12ge0  26473  bcmono  27244  n0cutlt  28355  bdayfin  28483  iswlkg  29687  usgrwwlks2on  30031  umgrwwlks2on  30032  clwlkclwwlkfo  30084  3cyclfrgrrn1  30360  grpodivf  30613  ipf  30788  shintcli  31404  spanuni  31619  adjadj  32011  unopadj2  32013  hmopadj  32014  hmopbdoptHIL  32063  resvsca  33413  resvlem  33414  submateq  33966  esumcocn  34237  bnj1379  34986  bnj571  35062  bnj594  35068  bnj580  35069  bnj600  35075  bnj1189  35165  bnj1321  35183  bnj1384  35188  f1resrcmplf1dlem  35242  trssfir1om  35267  fineqvinfep  35281  trssfir1omregs  35292  cplgredgex  35315  cusgr3cyclex  35330  loop1cycl  35331  umgr2cycllem  35334  umgr2cycl  35335  acycgr2v  35344  cusgracyclt3v  35350  climuzcnv  35865  fness  36543  bj-idreseq  37363  bj-imdiridlem  37386  neificl  37950  metf1o  37952  isismty  37998  ismtybndlem  38003  ablo4pnp  38077  divrngcl  38154  keridl  38229  prnc  38264  lsmsatcv  39266  llncvrlpln2  39813  lplncvrlvol2  39871  linepsubN  40008  pmapsub  40024  dalawlem10  40136  dalawlem13  40139  dalawlem14  40140  dalaw  40142  diaf11N  41305  dibf11N  41417  ismrcd1  42936  ismrcd2  42937  mzpincl  42972  mzpadd  42976  mzpmul  42977  pellfundge  43120  imasgim  43338  sqrtcval  43878  stoweidlem2  46242  stoweidlem17  46257  imaelsetpreimafv  47637  opnneir  49148  i0oii  49161  io1ii  49162