Theorem 3expia 1121

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	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:  ad5ant125  1368  mp3an3  1452  3gencl  3481  vtocl3gaf  3533  vtocl3ga  3535  moi  3673  disji  5080  disjord  5084  3optocl  5718  sossfld  6141  f1oresrab  7069  f1cdmsn  7225  soisores  7270  isomin  7280  isofrlem  7283  ovmpos  7503  ov2gf  7504  ndmovord  7545  nnsuc  7823  poxp  8067  frpoins3xp3g  8080  brtpos  8174  dfsmo2  8276  smoiun  8290  smoord  8294  smogt  8296  omeulem1  8506  omeu  8509  oewordi  8515  uniinqs  8730  mapvalg  8769  pmvalg  8770  elmapg  8772  xpdom3  8999  mapdom3  9073  sdomdomtrfi  9121  domsdomtrfi  9122  php  9127  php3  9129  nndomog  9133  onomeneq  9134  sucdom  9139  unxpdomlem3  9153  isinf  9160  f1finf1o  9168  isfinite2  9193  prfi  9219  ordiso  9413  cnfcom3clem  9606  r111  9679  tskwe  9854  pr2ne  9907  infxpenlem  9915  dfac8alem  9931  infdif  10110  infdif2  10111  cff1  10160  coflim  10163  cfslbn  10169  cfslb2n  10170  cofsmo  10171  cfsmolem  10172  cfcoflem  10174  fin23lem27  10230  isf32lem9  10263  isf34lem6  10282  axcc2lem  10338  domtriomlem  10344  axdc4lem  10357  zorn2lem2  10399  axdclem2  10422  konigthlem  10470  gchen1  10527  gchen2  10528  gchpwdom  10572  gchaleph  10573  winainflem  10595  tskcard  10683  gruiun  10701  gruen  10714  intgru  10716  grudomon  10719  grur1a  10721  grutsk1  10723  nqereu  10831  nqereq  10837  ltsonq  10871  prlem934  10935  reclem3pr  10951  1re  11123  axsup  11199  addlid  11307  recex  11760  lemul1a  11986  lt2msq  12018  fimaxre2  12078  zdiv  12553  zextlt  12557  prime  12564  uzind2  12576  fzind  12581  lbzbi  12840  qbtwnxr  13106  qextltlem  13108  xralrple  13111  xltneg  13123  xlt2add  13166  supxrgtmnf  13235  ixxub  13273  ixxlb  13274  ioo0  13277  ico0  13298  ioc0  13299  icc0  13300  iocssre  13334  icossre  13335  iccssre  13336  fzen  13448  expclzlem  13997  expaddz  14020  expmulz  14022  hashgadd  14291  hashunsngx  14307  hashgt23el  14338  elovmpowrd  14472  pfxnd0  14603  ccatopth2  14631  pfxccatin12  14647  cshf1  14724  shftuz  14983  cau3lem  15269  caubnd  15273  climuni  15466  lo1resb  15478  o1resb  15480  o1of2  15527  o1add  15528  o1mul  15529  o1sub  15530  ntrivcvgmul  15816  eflt  16033  moddvds  16181  dvdscmulr  16202  dvdsmulcr  16203  dvdsle  16228  divalglem8  16318  divalgb  16322  ndvdssub  16327  bitsfzo  16353  gcdcllem1  16417  gcdcllem3  16419  dvdsgcd  16462  nn0rppwr  16479  nn0expgcd  16482  lcmgcdlem  16524  lcmfeq0b  16548  qredeu  16576  isprm3  16601  prmdvdsexpr  16635  prmexpb  16637  eulerthlem2  16700  fermltl  16702  coprimeprodsq  16727  pythagtrip  16753  pcprendvds  16759  pcpremul  16762  pcdvdsb  16788  pc2dvds  16798  4sqlem12  16875  4sqlem18  16881  vdwlem10  16909  cshwshashlem3  17016  xpsrnbas  17483  ismred  17512  mrieqv2d  17553  iscatd  17587  isfuncd  17780  fthestrcsetc  18064  fthsetcestrc  18079  poslubd  18325  dirtr  18516  mulgaddcom  19019  ghmrn  19149  pmtrprfv3  19374  mndodcongi  19463  oddvdsnn0  19464  oddvds  19467  odcl2  19485  odhash3  19496  gexdvds  19504  pgpfi  19525  lsmss1b  19586  lsmss2b  19588  efgsrel  19654  efgred  19668  cntzcmn  19760  cyggenod  19804  lt6abl  19815  gsumcom2  19895  pgpfac1lem2  19997  pgpfac1lem3  19999  dvdsunit  20306  unitmulclb  20308  irredrmul  20354  isabvd  20736  lmodvsdi  20827  lss0cl  20889  islbs3  21101  lbsextlem2  21105  xrsdsreclblem  21358  psrbaglefi  21873  mvrf1  21932  coe1fzgsumd  22239  gsummoncoe1  22243  evl1gsumd  22292  scmataddcl  22451  scmatsubcl  22452  mdetunilem9  22555  mdetuni0  22556  mdetmul  22558  m2cpmrngiso  22693  pm2mpf1  22734  opnnei  23055  neindisj2  23058  cncls2  23208  cncls  23209  cnntr  23210  cnpresti  23223  cnprest  23224  lmcnp  23239  isreg2  23312  ordthauslem  23318  unconn  23364  2ndc1stc  23386  kgen2ss  23490  ptclsg  23550  cnmptcom  23613  kqfvima  23665  hmeof1o  23699  fbncp  23774  fbfinnfr  23776  trfbas2  23778  isufil2  23843  ufprim  23844  trufil  23845  filufint  23855  hausflim  23916  flimrest  23918  flimcls  23920  cnpfcf  23976  alexsubALT  23986  tmdgsum  24030  opnsubg  24043  cldsubg  24046  qustgpopn  24055  tsmsxp  24090  blpnf  24332  blssps  24359  blss  24360  blssec  24370  neibl  24436  prdsxmslem2  24464  xrsmopn  24748  metnrm  24798  climcncf  24840  iccpnfhmeo  24890  xrhmeo  24891  bndth  24904  cphsqrtcl3  25134  iscau2  25224  iscmet3lem2  25239  bcthlem5  25275  bcth3  25278  ishl2  25317  ivthlem1  25399  cmmbl  25482  iundisj2  25497  voliunlem2  25499  mbfaddlem  25608  itg2itg1  25684  itg2seq  25690  itg2mulclem  25694  cnplimc  25835  dvres2  25860  deg1nn0clb  26042  deg1lt0  26043  deg1ge  26050  plypf1  26164  plyadd  26169  plymul  26170  coeeu  26177  dgrub2  26187  coeidlem  26189  coeid3  26192  coemullem  26202  coe11  26205  coemulhi  26206  coemulc  26207  dgreq0  26218  dgrlt  26219  dgradd2  26221  vieta1lem2  26266  tanord1  26493  tanord  26494  logccne0  26534  cxpeq0  26634  cxpmul2z  26647  cxpcn3lem  26704  rtprmirr  26717  relogbzcl  26731  angpieqvd  26788  o1cxp  26932  scvxcvx  26943  chtublem  27169  bposlem3  27244  lgsqr  27309  2sqnn  27397  dchrisumlema  27446  dchrisumlem2  27448  ostth2lem3  27593  nosepon  27624  noextenddif  27627  nolesgn2o  27630  nogesgn1o  27632  nosepne  27639  nodense  27651  onnolt  28223  onslt  28224  onsiso  28225  bdayn0p1  28314  bdayn0sf1o  28315  tghilberti2  28636  inagswap  28839  f1otrg  28869  brbtwn2  28904  axpasch  28940  axcontlem4  28966  axcontlem5  28967  upgredg2vtx  29140  usgredg2vtxeuALT  29221  sizusglecusg  29463  upgredginwlk  29635  frgrwopreg1  30319  frgrwopreg2  30320  frgrregorufrg  30327  lpni  30481  ipasslem5  30836  htthlem  30918  omlsii  31404  spansni  31558  spansneleq  31571  elspansn4  31574  sumspansn  31650  homco1  31802  homulass  31803  mdsl0  32311  ssdmd1  32314  ssdmd2  32315  cvdmd  32338  chirredlem2  32392  atdmd  32399  atmd2  32401  disjif  32579  iundisj2f  32591  isoun  32707  preiman0  32715  padct  32725  iocinioc2  32787  iundisj2fi  32805  sgn3da  32843  sgnnbi  32847  sgnpbi  32848  indpi1  32869  archiabllem1a  33201  archiabllem2a  33204  slmdvsdi  33225  ordtconnlem1  34009  measinblem  34305  measres  34307  measdivcstALTV  34310  mbfmco2  34350  orvclteinc  34561  bnj605  34991  bnj607  35000  bnj964  35027  bnj1033  35053  bnj1128  35074  bnj1137  35079  bnj1136  35081  bnj1413  35119  bnj60  35146  rankfilimb  35185  r1filim  35187  fineqvac  35211  fineqvnttrclselem3  35215  fineqvnttrclse  35216  cusgredgex  35238  subgrwlk  35248  acycgr1v  35265  cvmlift2lem10  35428  msubvrs  35676  wsuclem  35939  dfrdg4  36067  brcolinear2  36174  brsegle2  36225  nn0prpw  36439  ntruni  36443  clsint2  36445  fnessref  36473  fnemeet2  36483  fnejoin2  36485  limsucncmpi  36561  ee7.2aOLD  36577  bj-idreseq  37279  dissneqlem  37457  isbasisrelowllem1  37472  isbasisrelowllem2  37473  icoreclin  37474  poimirlem9  37742  poimirlem30  37763  poimirlem32  37765  areacirc  37826  filbcmb  37853  mettrifi  37870  heiborlem8  37931  heiborlem10  37933  heibor  37934  riscer  38101  igenval2  38179  lshpcmp  39160  eqlkr  39271  lkrlsp2  39275  lkrshp  39277  cvrnbtwn2  39447  cvlexch3  39504  cvlexch4N  39505  cvlatexchb1  39506  cvlsupr3  39516  exatleN  39576  cvratlem  39593  atcvrj2b  39604  cvrat3  39614  cvrat4  39615  athgt  39628  ps-1  39649  ps-2  39650  3atlem5  39659  3at  39662  llnneat  39686  llnmlplnN  39711  lplnneat  39717  lplnnelln  39718  islpln2a  39720  lplnriaN  39722  lplnribN  39723  lplnexllnN  39736  2llnjaN  39738  lvolnle3at  39754  lvolneatN  39760  lvolnelln  39761  lvolnelpln  39762  islvol2aN  39764  dalem62  39906  pmapglb2N  39943  pmapglb2xN  39944  lncmp  39955  paddasslem14  40005  paddasslem15  40006  pmod2iN  40021  hlmod1i  40028  pclfinclN  40122  osumcllem8N  40135  pexmidlem4N  40145  pl42lem1N  40151  pl42lem4N  40154  lhpexle1  40180  lhpexle2lem  40181  lhpmcvr5N  40199  lhpmcvr6N  40200  ltrneq  40321  trlnidatb  40349  cdleme0ex2N  40396  cdleme27a  40539  cdleme17d3  40668  cdlemeg46gfre  40704  cdleme48gfv1  40708  cdlemeg49lebilem  40711  cdlemf2  40734  cdlemf  40735  cdlemfnid  40736  trlord  40741  cdlemg31c  40871  cdlemg35  40885  trlcone  40900  tendoeq2  40946  cdlemj3  40995  cdlemk26b-3  41077  cdlemk33N  41081  cdleml3N  41150  cdlemn  41384  dih1dimb2  41413  dihord5apre  41434  dihmeetlem1N  41462  dihglblem5apreN  41463  dihglblem2N  41466  dihglblem3N  41467  dihmeetlem13N  41491  dihmeetlem15N  41493  dihatexv  41510  hdmap14lem12  42051  uzindd  42143  lcmineqlem1  42195  sticksstones1  42312  dvdsexpnn0  42504  frlmfzowrdb  42674  oddcomabszz  43101  jm2.19lem4  43149  fiuneneq  43349  idomsubgmo  43350  omcl2  43490  pwinfi3  43720  gneispa  44287  mnringmulrcld  44385  grumnudlem  44442  ismnushort  44458  binomcxplemnn0  44506  addrcom  44631  int3  44769  suctrALT  44982  suctrALTcf  45078  suctrALT3  45080  chordthmALT  45089  iunconnlem2  45091  relpmin  45109  relpfrlem  45110  stoweidlem26  46186  stoweidlem34  46194  issald  46493  goldbachth  47709  grlimgrtri  48165  nnsgrp  48339  ply1mulgsumlem1  48548  lubsscl  49121  glbsscl  49122