Theorem 3expib 1121

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 1118	. 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  1418  mob  3725  dfss2  3980  eqbrrdva  5882  f1oiso2  7371  frxp  8149  onfununi  8379  smoel2  8401  smoiso2  8407  3ecoptocl  8847  ssfi  9211  f1domfi  9218  rex2dom  9279  fodomfib  9366  dffi2  9460  elfiun  9467  dif1card  10047  infxpenlem  10050  cfeq0  10293  cfsuc  10294  cfflb  10296  cfslb2n  10305  cofsmo  10306  domtriomlem  10479  axdc3lem4  10490  axdc4lem  10492  ttukey2g  10553  tskxpss  10809  grudomon  10854  elnpi  11025  dedekind  11421  nn0n0n1ge2b  12592  fzind  12713  suprzcl2  12977  icoshft  13509  fzen  13577  hashgt23el  14459  hashfundm  14477  hashbclem  14487  seqcoll  14499  relexpsucl  15066  relexpsucr  15067  relexpfld  15084  shftuz  15104  mulgcd  16581  algcvga  16612  lcmneg  16636  ressbas  17279  ressbasOLD  17280  resseqnbas  17286  resslemOLD  17287  ressress  17293  psss  18637  tsrlemax  18643  isnmgm  18669  gsummgmpropd  18706  issgrpd  18755  iscmnd  19826  ring1ne0  20312  unitmulclb  20397  isdrngd  20781  isdrngdOLD  20783  abvn0b  20853  issrngd  20872  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  isphld  21689  mpfaddcl  22146  mpfmulcl  22147  pf1addcl  22372  pf1mulcl  22373  fitop  22921  hausnei2  23376  ordtt1  23402  locfincmp  23549  basqtop  23734  filfi  23882  fgcl  23901  neifil  23903  filuni  23908  cnextcn  24090  prdsmet  24395  blssps  24449  blss  24450  metcnp3  24568  hlhil  25490  volsup2  25653  sincosq1sgn  26554  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  sinq12ge0  26564  bcmono  27335  iswlkg  29645  umgrwwlks2on  29986  clwlkclwwlkfo  30037  3cyclfrgrrn1  30313  grpodivf  30566  ipf  30741  shintcli  31357  spanuni  31572  adjadj  31964  unopadj2  31966  hmopadj  31967  hmopbdoptHIL  32016  resvsca  33335  resvlem  33336  resvlemOLD  33337  submateq  33769  esumcocn  34060  bnj1379  34822  bnj571  34898  bnj594  34904  bnj580  34905  bnj600  34911  bnj1189  35001  bnj1321  35019  bnj1384  35024  f1resrcmplf1dlem  35078  cplgredgex  35104  cusgr3cyclex  35120  loop1cycl  35121  umgr2cycllem  35124  umgr2cycl  35125  acycgr2v  35134  cusgracyclt3v  35140  climuzcnv  35655  fness  36331  bj-idreseq  37144  bj-imdiridlem  37167  neificl  37739  metf1o  37741  isismty  37787  ismtybndlem  37792  ablo4pnp  37866  divrngcl  37943  keridl  38018  prnc  38053  lsmsatcv  38991  llncvrlpln2  39539  lplncvrlvol2  39597  linepsubN  39734  pmapsub  39750  dalawlem10  39862  dalawlem13  39865  dalawlem14  39866  dalaw  39868  diaf11N  41031  dibf11N  41143  ismrcd1  42685  ismrcd2  42686  mzpincl  42721  mzpadd  42725  mzpmul  42726  pellfundge  42869  imasgim  43088  sqrtcval  43630  stoweidlem2  45957  stoweidlem17  45972  imaelsetpreimafv  47319  opnneir  48702  i0oii  48715  io1ii  48716